--- a/system-f.agda	Thu Mar 20 06:25:38 2014 +0700
+++ b/system-f.agda	Thu Mar 20 10:23:54 2014 +0700
@@ -145,13 +145,27 @@
 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 {l} {X} x y = R {l} {Int {l} {X}} y ( λ z -> λ w -> S z ) x
+sum x y = R y ( λ z -> λ w -> S z ) x
+
+mul : Int -> Int -> Int 
+mul  x y = R Zero ( λ (z : Int) -> λ (w : Int) -> sum y 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
+
+-- lemma14 : (x y : Int) -> mul x y  ≡ mul y x
+-- lemma14 x y = {!!}
 
-mul : {l : Level} {X : Set l} -> Int -> Int -> Int
-mul x y = R Zero ( λ (z : Int) -> λ (w : Int) -> sum y z ) x
+lemma15 : {l : Level} {X : Set l} (x y : Int {l} {X}) -> mul n2 n3  ≡ mul n3 n2
+lemma15 x y = refl
 
-fact : {l : Level} {X : Set l} -> Int -> Int
-fact  {l} {X} n = R  (S Zero) (λ ( z : Int) -> λ (w : Int) -> mul (S w) z ) n
+lemma16 : {l : Level} {X U : Set l} -> (u : U ) -> (v : U -> Int {l} {X} ->  U ) -> R u v Zero ≡ u
+lemma16 u v = refl
+
+-- 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
+-- lemma17 u v t = refl
+
+-- 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