--- a/system-f.agda	Fri Apr 18 20:19:32 2014 +0900
+++ b/system-f.agda	Sat Apr 19 00:29:39 2014 +0900
@@ -133,25 +133,28 @@
 R : {l : Level} { U X : Set l}   → U → ( U → Int X →  U ) → Int _ → U 
 R {l} {U} {X} u v t =  π1 ( It {suc l} {U ×  Int X} (< u , Zero >) (λ (x : U × Int X) →  < v (π1 x) (π2 x) , S (π2 x) > ) t ) 
 
--- ItInt : {l : Level} {U : Set l} → Int U → ( Int U → Int U ) → Int U → Int U
--- ItInt {l} {U} u f t = λ t u f
+ItInt : {l : Level} {X : Set l} → Int X → ( Int X → Int X ) → Int X → Int X
+ItInt {l} {X} u f t = λ z s → t (u z s) ( λ w → (f (λ z' s' → w )) z s )
 
--- RInt : {l : Level} { U X : Set l}   → Int U → ( Int U → Int X →  Int U ) → Int U → Int U 
--- RInt {l} {U} {X} u v t =  π1 ( It {suc l} {Int U ×  Int X} (< u , Zero >) (λ (x : Int U × Int X) →  < v (π1 x) (π2 x) , S (π2 x) > ) t ) 
+-- RInt : {l : Level} { U : Set l}   → Int U → ( Int U → Int U →  Int U ) → Int U → Int U 
+-- RInt {l} {U} u v t =  π1 ( ItInt {suc l} {Int U ×  Int U} (< u , Zero >) (λ (x : Int U × Int U) →  < v (π1 x) (π2 x) , S (π2 x) > ) t ) 
 
 -- bad adder which modifies input type
 add' : {l : Level} {X : Set l} → Int (Int X) → Int X → Int X
 add' x y = It y S x
 
 add : {l : Level} {X : Set l} → Int X → Int X → Int X
-add x y = λ z t → x (y z t) t
+add x y = λ z s → x (y z s) s
 
 -- bad adder which modifies input type
 mul' : {l : Level } {X : Set l} → Int X → Int (Int X) → Int X
 mul' {l} {X} x y = It Zero (add x) y
 
 mul : {l : Level } {X : Set l} → Int X → Int X → Int X
-mul {l} {X} x y = λ z t → x z ( λ w → y w t )
+mul {l} {X} x y = λ z s → x z ( λ w → y w s )
+
+mul'' : {l : Level } {X : Set l} → Int X → Int X → Int X
+mul'' {l} {X} x y = ItInt Zero (add x) y
 
 fact : {l : Level} {X : Set l} → Int _ → Int X
 fact  {l} {X} n = R (S Zero) (λ z → λ w → mul z (S w)) n
@@ -159,12 +162,16 @@
 lemma13' : {l : Level} {X : Set l} → fact {l} {X} n4 ≡ mul n4 ( mul n2 n3)
 lemma13' = refl
 
+
 -- lemma14 : {l : Level} {X : Set l} → (x y : Int X) → mul x y  ≡ mul y x
 -- lemma14 x y = It {!!} {!!} {!!}
 
 lemma15 : {l : Level} {X : Set l} (x y : Int X) → mul {l} {X} n2 n3  ≡ mul {l} {X} n3 n2
 lemma15 x y = refl
 
+lemma15' : {l : Level} {X : Set l} (x y : Int 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 X →  U ) → R u v Zero ≡ u
 lemma16 u v = refl