# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1396942268 -32400
# Node ID 4977c5873660cdd95cca583f7ca6ef5ee3687d65
# Parent  627da4867e5bca88a2f62e534a59c0f34e25e7b7
Add lemma-it of Int, but has yellow

diff -r 627da4867e5b -r 4977c5873660 systemF.agda
--- a/systemF.agda	Tue Apr 08 15:29:46 2014 +0900
+++ b/systemF.agda	Tue Apr 08 16:31:08 2014 +0900
@@ -93,10 +93,10 @@
 
 -- Int
 
-Int : {l : Level} {X : Set l} -> Set l
+Int : {l : Level} -> {X : Set l} -> Set l
 Int {l} {X} = X -> (X -> X) -> X
 
-O : {l : Level} -> {X : Set l} -> Int 
+O : {l : Level} -> {X : Set l} -> Int
 O {l} {X} =  \(x : X) -> \(y : X -> X) -> x
 
 S : {l : Level} -> {X : Set l} -> Int -> Int
@@ -112,4 +112,7 @@
 lemma-it-s-o = refl
 
 g : {l : Level} -> {U : Set l} -> {f : U -> Int {l} {U} -> U} -> (U × Int) -> (U × Int)
-g {l} {U} {f} = \x -> < (f (π1 x) (π2 x)) , S (π2 x) >
\ No newline at end of file
+g {l} {U} {f} = \x -> < (f (π1 x) (π2 x)) , S (π2 x) >
+
+lemma-it : {l : Level} {U : Set l} {u : U} {n : Int} {f : U -> Int -> U} -> g {l} {U} {f} < u , n > ≡ < f u n , S n >
+lemma-it = refl