# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1397097037 -32400
# Node ID 93705fd8f5771c057c9966d5bb1b66a6631de79a
# Parent  8c735b9ebf5af2a99764c54e52d6cacb8ec164fe
Add comment to g

diff -r 8c735b9ebf5a -r 93705fd8f577 systemF.agda
--- a/systemF.agda	Tue Apr 08 17:18:00 2014 +0900
+++ b/systemF.agda	Thu Apr 10 11:30:37 2014 +0900
@@ -117,5 +117,6 @@
 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) >
 
-lemma-it-n : {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-n = refl
\ No newline at end of file
+-- cannot prove general Int
+-- lemma-it-n : {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-n = refl