--- a/system-f.agda	Mon Mar 24 16:45:25 2014 +0700
+++ b/system-f.agda	Sat Mar 29 17:12:33 2014 +0900
@@ -149,6 +149,13 @@
 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 ? ? )
+
 fact : {l : Level} {X : Set l} → Int _ → Int X
 fact  {l} {X} n = R (S Zero) (λ z → λ w → mul z (S w) ) n