--- a/system-f.agda	Thu Mar 20 11:32:47 2014 +0700
+++ b/system-f.agda	Fri Mar 21 17:30:46 2014 +0700
@@ -125,6 +125,9 @@
 S : {l : Level } -> { X : Set l } -> Int -> Int 
 S {l} {X} t = \(x : X) -> \(y : X -> X ) -> y ( t x y )
 
+n0 : {l : Level} {X : Set l} -> Int {l} {X}
+n0 = Zero
+
 n1 : {l : Level } -> { X : Set l } -> Int {l} {X}
 n1 {l} {X} = \(x : X ) -> \(y : X -> X ) -> y x
 
@@ -145,18 +148,24 @@
 R {l} {U} u v t =  π1 ( It {suc l} {U  ×  Int} (< u , Zero >) (λ (x : U × Int) →  < v (π1 x) (π2 x) , S (π2 x) > ) t ) 
 
 sum : {l : Level} {X : Set l} -> Int -> Int {l} {X} -> Int
-sum x y = R y ( λ z -> λ w -> S z ) x
+sum x y = It y ( λ z -> S z ) x
+
+mul : {l : Level } {X : Set l} -> Int {l} {_} -> Int  -> Int {l} {X}
+mul  x y = It Zero ( λ (z : Int) -> sum y z ) x
 
-mul : Int -> Int -> Int 
-mul  x y = R Zero ( λ (z : Int) -> λ (w : Int) -> sum y z ) x
+copyInt : {l : Level } {X : Set l} -> Int {l} {_} -> Int {l} {X}
+copyInt  x = It Zero ( λ (z : Int) -> S z ) x
 
--- fact : {l : Level} {X : Set l} -> Int -> Int
--- fact  {l} {X} n = R  (S Zero) (λ ( z : Int) -> λ (w : Int) -> mul (S w) z ) n
+-- fact : {l : Level} {X X' : Set l} -> Int -> Int {l} {_}
+-- fact  {l} {X} {X'} n = R  (S Zero) (λ ( z w : Int) -> mul {l} {_} z (S w) ) n
+
+-- lemma13' : fact n3 ≡ mul n1 ( mul n2 n3)
+-- lemma13' = refl
 
 -- lemma14 : (x y : Int) -> mul x y  ≡ mul y x
--- lemma14 x y = {!!}
+-- lemma14 x y = It {!!} {!!} {!!}
 
-lemma15 : {l : Level} {X : Set l} (x y : Int {l} {X}) -> mul n2 n3  ≡ mul n3 n2
+lemma15 : {l : Level} {X : Set l} (x y : Int {l} {X}) -> mul {l} {X} n2 n3  ≡ mul {l} {X} n3 n2
 lemma15 x y = refl
 
 lemma16 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int {l} {X} ->  U ) -> R u v Zero ≡ u
@@ -191,9 +200,12 @@
 Nullp : {l : Level} {U : Set (suc l)} { X : Set (suc l)} -> List {suc l} {U} {Bool {l}} -> 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} -> List {l} {U} {X} -> List {l} {U} {X}
+Append : {l : Level} {U : Set l} {X : Set l} -> List {l} {U} {_} -> List {l} {U} {X} -> List {l} {U} {_}
 Append {l} {U} {X} x y = ListIt {l} {U} {_} {X} y (\u w -> Cons u w) x
 
+-- lemma18 : Append l1 l2 ≡ Cons n1 ( Cons n2 Nil )
+-- lemma18 = 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}