This commit was manufactured by cvs2svn to create branch 'moogle'.

[helm.git] / helm / EXPORT / exportprove / prove / provaF.v

diff --git a/helm/EXPORT/exportprove/prove/provaF.v b/helm/EXPORT/exportprove/prove/provaF.v
deleted file mode 100644 (file)
index 072010f..0000000
--- a/helm/EXPORT/exportprove/prove/provaF.v
+++ /dev/null
@@ -1,33 +0,0 @@
-Definition int := (A:Prop)(A->A)->A->A.
-
-Definition O := [A:Prop][s:A->A][o:A]o.
-
-Definition S := [n:int][A:Prop][s:A->A][o:A](s (n A s o)).
-
-Definition Uno := [A:Prop][s:A->A][o:A](s o).
-
-Definition Due := [A:Prop][s:A->A][o:A](s (s o)).
-
-Definition Tre := [A:Prop][s:A->A][o:A](s (s (s o))).
-
-Definition id := [A:Prop][x:A]x.
-
-Definition id_Due := (id int Due).
-
-Definition difficult := ((S Due) (int -> int) (id (int -> int)) (id int)).
-
-Definition is_Zero := [n:int](n int [_:int]Uno O).
-
-Definition couple := [A:Prop][x:A][y:A][z:A->A->A](z x y).
-
-Definition Couple := [A:Prop](z:A->A->A)A.
-
-Definition fst := [A:Prop][x:A][y:A]x.
-
-Definition snd := [A:Prop][x:A][y:A]y.
-
-Definition next : (Couple int) -> (Couple int) := [x:(Couple int)](couple int (x (snd int)) (S (x (snd int)))).
-
-Definition pred := [n:int]((n (Couple int) next (couple int O O))(fst int)).
-
-Definition test := (((pred Tre) (int -> int))(id (int->int)) (id int)).