--- a/system-f.agda	Sat Mar 22 09:31:46 2014 +0700
+++ b/system-f.agda	Sat Mar 22 10:22:25 2014 +0700
@@ -1,44 +1,24 @@
 open import Level
 open import Relation.Binary.PropositionalEquality
 
-module system-f {l : Level} where
-
-postulate A : Set
-postulate B : Set
+module system-f  where
 
-data _∨_  (A B : Set) : Set where
-  or1 : A -> A ∨ B
-  or2 : B -> A ∨ B
+Bool : {l : Level} {X : Set l} -> Set l
+Bool = \{l : Level} -> \{X : Set l} -> X -> X -> X
 
-lemma01 : A -> A ∨ B
-lemma01 a = or1 a
-
-lemma02 : B -> A ∨ B
-lemma02 b = or2 b
+T : {l : Level} {X : Set l} -> Bool {l} {X}
+T {l} {X} = \(x y : X) -> x
 
-lemma03 : {C : Set} -> (A ∨ B) -> (A -> C) -> (B -> C) -> C
-lemma03 (or1 a) ac bc = ac a
-lemma03 (or2 b) ac bc = bc b
-
-postulate U : Set l
-postulate V : Set l
-
-
-Bool = \{l : Level} -> {X : Set l} -> X -> X -> X
+F : {l : Level} {X : Set l} -> Bool {l} {X}
+F {l} {X} = \(x y : X) -> y
 
-T : {l : Level} -> Bool
-T {l} = \{X : Set l} -> \(x y : X) -> x
+D : {l : Level} -> {U : Set l} -> U -> U -> Bool {l} {U} -> U
+D {l} {U} u v t = t u v
 
-F : {l : Level} -> Bool
-F {l}  = \{X : Set l} -> \(x y : X) -> y
-
-D : {l : Level} -> {U : Set l} -> U -> U -> Bool -> U
-D {l} {U} u v t = t {U} u v
-
-lemma04 : {u v : U} -> D u v T ≡  u
+lemma04 : {l : Level} { U : Set l} {u v : U} -> D {_} {U} u v (T {_} {U} ) ≡  u
 lemma04 = refl
 
-lemma05 : {u v : U} -> D u v F ≡  v
+lemma05 : {l : Level} { U : Set l} {u v : U} -> D {_} {U} u v (F {_} {U} ) ≡  v
 lemma05 = refl
 
 _×_ : {l : Level} -> Set l -> Set l ->  Set (suc l)
@@ -53,13 +33,13 @@
 π2 : {l : Level} {U V : Set l} -> (U ×  V) -> V
 π2 {l} {U} {V}  t = t {V} (\(x : U) -> \(y : V) -> y)
 
-lemma06 : {U V : Set l } -> {u : U } -> {v : V} -> π1 ( < u , v > ) ≡  u
+lemma06 : {l : Level} {U V : Set l } -> {u : U } -> {v : V} -> π1 ( < u , v > ) ≡  u
 lemma06 = refl
 
-lemma07 : {U V : Set l } -> {u : U } -> {v : V} -> π2 ( < u , v > ) ≡  v
+lemma07 : {l : Level} {U V : Set l } -> {u : U } -> {v : V} -> π2 ( < u , v > ) ≡  v
 lemma07 = refl
 
-hoge : {U V : Set l} -> U -> V  -> (U ×  V)
+hoge : {l : Level} {U V : Set l} -> U -> V  -> (U ×  V)
 hoge u v = < u , v >
 
 -- lemma08 :  (t : U ×  V)  -> < π1 t  , π2 t > ≡ t
@@ -94,22 +74,22 @@
 -- lemma103 : {l : Level} {U V : Set l} -> (u : U) -> (t : Emp {l} {_} ) -> (ε (U -> V) t) u ≡ ε V t
 -- lemma103 u t = refl
 
-_+_  : Set l -> Set l -> Set (suc l)
-U + V = {X : Set l} -> ( U -> X ) -> (V -> X) -> X
+_+_  : {l : Level} -> Set l -> Set l -> Set (suc l)
+_+_ {l} U V = {X : Set l} -> ( U -> X ) -> (V -> X) -> X
 
-ι1 : {U V : Set l} ->  U ->  U + V
-ι1 {U} {V} u = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> x u
+ι1 : {l : Level } {U V : Set l} ->  U ->  U + V
+ι1 {l} {U} {V} u = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> x u
 
-ι2 : {U V : Set l} ->  V ->  U + V
-ι2 {U} {V} v = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> y v
+ι2 : {l : Level } {U V : Set l} ->  V ->  U + V
+ι2 {l} {U} {V} v = \{X} -> \(x : U -> X) -> \(y : V -> X ) -> y v
 
-δ : { U V R S : Set l } -> (R -> U) -> (S -> U) -> ( R + S ) -> U
-δ  {U} {V} {R} {S} u v t = t {U} (\(x : R) -> u x) ( \(y : S) -> v y)
+δ : {l : Level} { U V R S : Set l } -> (R -> U) -> (S -> U) -> ( R + S ) -> U
+δ {l} {U} {V} {R} {S} u v t = t {U} (\(x : R) -> u x) ( \(y : S) -> v y)
 
-lemma11 : { U V R S : Set l } -> (u : R -> U ) (v : S -> U ) -> (r : R) -> δ  {U} {V} {R} {S} u v ( ι1 r )  ≡ u r
+lemma11 : {l : Level} { U V R S : Set _ } -> (u : R -> U ) (v : S -> U ) -> (r : R) -> δ {l} {U} {V} {R} {S} u v ( ι1 r )  ≡ u r
 lemma11 u v r =  refl
 
-lemma12 : { U V R S : Set l } -> (u : R -> U ) (v : S -> U ) -> (s : S) -> δ  {U} {V} {R} {S} u v ( ι2 s )  ≡ v s
+lemma12 : {l : Level} { U V R S : Set _ } -> (u : R -> U ) (v : S -> U ) -> (s : S) -> δ {l} {U} {V} {R} {S} u v ( ι2 s )  ≡ v s
 lemma12 u v s =  refl
 
 
@@ -120,6 +100,7 @@
 <<_,_>> {l} {U} {V} u v = \{X} -> \(x : U -> V -> X) -> x u v
 
 
+Int : {l : Level } { X : Set l } -> Set l
 Int = \{l : Level } -> \{ X : Set l } -> X -> ( X -> X ) -> X
 
 Zero : {l : Level } -> { X : Set l } -> Int 
@@ -179,8 +160,8 @@
 
 -- postulate lemma17 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int ->  U ) -> (t : Int ) -> R u v (S t) ≡ v ( R u v t ) t
 
-
-List = \{l : Level} -> \{ U X : Set l}  -> X -> ( U -> X ->  X ) -> X
+List : {l : Level} {U X : Set l} -> Set l
+List = \{l : Level} -> \{ U X : Set l}  -> X -> ( U -> X ->  X ) -> X 
 
 Nil : {l : Level} {U : Set l} {X : Set l} -> List {l} {U} {X}
 Nil {l} {U} {X} = \(x : X) -> \(y : U -> X -> X) -> x
@@ -197,10 +178,13 @@
 l2 : {l : Level} {X X' : Set l} -> List {l} {Int {l} {X}} {X'}
 l2 = Cons n2 l1
 
+l3 : {l : Level} {X X' : Set l} -> List {l} {Int {l} {X}} {X'}
+l3 = Cons n3 l2
+
 ListIt : {l : Level} {U W X : Set l} -> W -> ( U -> W -> W ) -> List {l} {U} {W} -> W
 ListIt {l} {U} {W} {X} w f t = t w f
 
-Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} -> List {suc l} {U} {Bool {l}} -> Bool
+Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} -> List {suc l} {U} {Bool {_} {X}} -> Bool {_} {_}
 Nullp {l} {U} {X} list = ListIt {suc l} {U} {Bool} {X} T (\u w -> F) list
 
 Append : {l : Level} {U : Set l} {X : Set l} -> List {l} {U} {_} -> List {l} {U} {X} -> List {l} {U} {_}
@@ -209,6 +193,12 @@
 lemma18 :{l : Level} {U : Set l} {X : Set l} -> Append {l} {Int {l} {U}} {X} l1 l2 ≡ Cons n1 (Cons n2 (Cons n1 Nil))
 lemma18 = refl
 
+Reverse : {l : Level} {U : Set l} {X : Set l} -> List {l} {U} {_} -> List {l} {U} {X}
+Reverse {l} {U} {X} x = ListIt {l} {U} {List {l} {U} {_}} {X} Nil ( \u w -> Append w (Cons u Nil) ) x
+
+lemma19 :{l : Level} {U : Set l} {X : Set l} -> Reverse {l} {Int {l} {U}} {X} l3 ≡ Cons n1 (Cons n2 (Cons n3 Nil))
+lemma19 = refl
+
 Tree = \{l : Level} -> \{ U X : Set l}  -> X -> ( (U -> X) ->  X ) -> X
 
 NilTree : {l : Level} {U : Set l} {X : Set l} -> Tree {l} {U} {X}