--- a/systemF.agda	Tue Apr 01 15:31:29 2014 +0900
+++ b/systemF.agda	Mon Apr 07 11:06:28 2014 +0900
@@ -89,3 +89,23 @@
 
 lemma-nabla : {X W : Set l} -> {x : X} -> {w : W} -> (∇_,_,_ {W} X {v x} x w) ⟨ X , (v x) ⟩ ≡ w
 lemma-nabla = refl
+
+
+-- Int
+
+Int = {X : Set} -> X -> (X -> X) -> X
+
+O : Int
+O = \{X : Set} -> \(x : X) -> \(y : X -> X) -> x
+
+S : Int -> Int
+S t = \{X : Set} -> \(x : X) -> \(y : X -> X) -> y (t {X} x y)
+
+It : {U : Set} -> (u : U) -> (U -> U) -> Int -> U
+It {U} u f t = t {U} u f
+
+lemma-it-o : {U : Set} -> {u : U} -> {f : U -> U} -> It u f O ≡ u
+lemma-it-o = refl
+
+lemma-it-s-o : {U : Set} -> {u : U} -> {f : U -> U} -> {t : Int} -> It u f (S t) ≡ f (It u f t)
+lemma-it-s-o = refl
\ No newline at end of file