lemTest not in prelude..

diff --git a/examples/bool.ctt b/examples/bool.ctt
index 71520f1bdce482f721437d859f8a7e2a7f7f4048..8e245107eb3b53c3ef73633d54547baceeee37a9 100644 (file)
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -41,6 +41,11 @@ boolEqF2 : Id U bool F2 =
   
 negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 neg
 
+
+lemTest (A : U) : (B : U) (p : Id U A B) (a : A) -> IdP p a (transport p a) =
+  J U A (\(B : U) (p : Id U A B) -> (a : A) -> IdP p a (transport p a)) (refl A)
+
+
 test : IdP boolEqF2 true one = <i> glueElem one [ (i = 0) -> true ]
 test1 : IdP boolEqF2 true one = lemTest bool F2 boolEqF2 true
 

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index b0fee3cb32f69b37a4a546394482ca5ae73d83cb..cb0f4b6a1dccde652c36e28b0d5262bb5d8b1adb 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -37,7 +37,3 @@ isoId (A B : U) (f : A -> B) (g : B -> A)
       (s : (y:B) -> Id B (f (g y)) y)
       (t : (x:A) -> Id A (g (f x)) x) : Id U A B =
       <i> glue B [ (i = 0) -> (A,(f,(g,(s,t)))) ]
-
-lemTest (A : U) : (B : U) (p : Id U A B) (a : A) -> IdP p a (transport p a) =
-  J U A (\(B : U) (p : Id U A B) -> (a : A) -> IdP p a (transport p a)) rem
-    where rem (a : A) : Id A a a = refl A a
\ No newline at end of file