X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FEXPORT%2Fexportprove%2Fprove%2FprovaF.v;fp=helm%2FEXPORT%2Fexportprove%2Fprove%2FprovaF.v;h=0000000000000000000000000000000000000000;hp=072010f0caf3e4fe2ee7bfda8cd2a978523689a5;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1

diff --git a/helm/EXPORT/exportprove/prove/provaF.v b/helm/EXPORT/exportprove/prove/provaF.v
deleted file mode 100644
index 072010f0c..000000000
--- 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)).