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

diff --git a/helm/EXPORT/exportprove/prove/provacofix.v b/helm/EXPORT/exportprove/prove/provacofix.v
deleted file mode 100644
index 199cadeb6..000000000
--- a/helm/EXPORT/exportprove/prove/provacofix.v
+++ /dev/null
@@ -1,45 +0,0 @@
-(* Let's define an infinite tree whose nodes are made of natural value and an *)
-(* infinite forest of infinite trees whose nodes ...                          *)
-
-(* (obbrobrio_tree n) is used to build such a tree whose root value is n and *)
-(* root forest is made of the corecursively defined tress whose roots values *)
-(* are (n+1), (n+2), ...                                                     *)
-
-(* To finish, we provide also some destructors and a funny (?!?) theorem     *)
-
-CoInductive tree : Set :=
-   node : nat -> forest -> tree      
-with forest : Set :=
-   nil : forest
- | cons : tree -> forest -> forest.
-
-CoFixpoint obbrobrio_tree : nat -> tree :=
- [n:nat]
-  (node n (obbrobrio_forest (S n) nil))
-with obbrobrio_forest : nat -> forest -> forest :=
- [n:nat][f:forest]
-  (cons (obbrobrio_tree n) (obbrobrio_forest (S n) f)).
-
-Definition root_value : tree -> nat :=
- [t:tree]
- Cases t of
-    (node n _) => n
- end.
-
-Definition root_forest : tree -> forest :=
- [t:tree]
- Cases t of
-    (node _ f) => f
- end.
-
-Definition root_tree : forest -> tree :=
- [f:forest]
- Cases f of
-    nil => (obbrobrio_tree (S (S (S O))))
-  | (cons t _) => t
- end.
-
-Theorem easy : (root_value (root_tree (root_forest (obbrobrio_tree O))))=(S O).
-Proof.
- Trivial.
-Qed.