X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Flist%2Flist.ma;h=19866cc2992499df10a53a9c0fba8766458c601f;hb=82baf094141d9ef518d681b8cebcc180bca14d2c;hp=c6fd212beca5b6f8b623b39cf95bee3508c48fac;hpb=96c91e470f670018df67c9cbff62fa06e3b57c5e;p=helm.git

diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma
index c6fd212be..19866cc29 100644
--- a/helm/software/matita/library/list/list.ma
+++ b/helm/software/matita/library/list/list.ma
@@ -109,8 +109,8 @@ with permut1 : list A -> list A -> Prop \def
   | step : \forall l1,l2:list A. \forall x,y:A. 
       permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).
 
-include "nat/nat.ma".  
-   
+(*
+
 definition x1 \def S O.
 definition x2 \def S x1.
 definition x3 \def S x2.
@@ -121,15 +121,9 @@ theorem tmp : permutation nat (x1 :: x2 :: x3 :: []) (x1 :: x3 :: x2 :: []).
   apply (step ? (x1::[]) [] x2 x3).
   qed. 
 
-
-(*
 theorem nil_append_nil_both:
   \forall A:Type.\forall l1,l2:list A.
     l1 @ l2 = [] \to l1 = [] \land l2 = [].
-*)
-
-(*
-include "nat/nat.ma".
 
 theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. 
 reflexivity.
@@ -139,6 +133,7 @@ theorem test_append: [O;O;O;O;O;O] = [O;O;O] @ [O;O] @ [O].
 simplify.
 reflexivity.
 qed.
+
 *)
 
 definition nth ≝