--- a/system-f.agda	Sat Mar 29 17:12:33 2014 +0900
+++ b/system-f.agda	Sat Mar 29 23:00:22 2014 +0900
@@ -134,7 +134,7 @@
 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} {U} u f t = λ t u f
 
 -- 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 ) 
@@ -146,18 +146,15 @@
 add : {l : Level} {X : Set l} → Int X → Int X → Int X
 add x y = λ z t → x (y z t) t
 
-mul : {l : Level } {X : Set l} → Int X → Int (Int X) → Int X
-mul {l} {X} x y = It Zero (add x) y
+-- 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
 
---   λ x y → y y y y x
---   λ x y → y y y x
---   λ z t →   (λ x y → y y y y x) (λ x y → y y y y x) (λ x y → y y y y x) t
---   λ z t →            t t t t             t t t t             t t t t    z
--- mul : {l : Level } {X : Set l} → Int X → Int X → Int X
--- mul {l} {X} x y = λ z t → x z ( λ w → 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 )
 
 fact : {l : Level} {X : Set l} → Int _ → Int X
-fact  {l} {X} n = R (S Zero) (λ z → λ w → mul z (S w) ) n
+fact  {l} {X} n = R (S Zero) (λ z → λ w → mul z (S w)) n
 
 lemma13' : {l : Level} {X : Set l} → fact {l} {X} n4 ≡ mul n4 ( mul n2 n3)
 lemma13' = refl