X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fesempi%2Felim2.cic;fp=helm%2FgTopLevel%2Fesempi%2Felim2.cic;h=0000000000000000000000000000000000000000;hb=869549224eef6278a48c16ae27dd786376082b38;hp=da77539661f9152f7dd894f06bbe12700b55d91f;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8;p=helm.git

diff --git a/helm/gTopLevel/esempi/elim2.cic b/helm/gTopLevel/esempi/elim2.cic
deleted file mode 100644
index da7753966..000000000
--- a/helm/gTopLevel/esempi/elim2.cic
+++ /dev/null
@@ -1,36 +0,0 @@
-alias nat        /Coq/Init/Datatypes/nat.ind#1/1
-alias eq         /Coq/Init/Logic/Equality/eq.ind#1/1
-alias eq_ind     /Coq/Init/Logic/Equality/eq_ind.con
-alias eqT        /Coq/Init/Logic_Type/eqT.ind#1/1
-alias O          /Coq/Init/Datatypes/nat.ind#1/1/1
-alias S          /Coq/Init/Datatypes/nat.ind#1/1/2
-alias plus       /Coq/Init/Peano/plus.con
-alias mult       /Coq/Init/Peano/mult.con
-alias le         /Coq/Init/Peano/le.ind#1/1
-alias lt         /Coq/Init/Peano/lt.con
-alias not        /Coq/Init/Logic/not.con
-alias and        /Coq/Init/Logic/Conjunction/and.ind#1/1
-alias prod       /Coq/Init/Datatypes/prod.ind#1/1 
-alias list       /Coq/Lists/PolyList/Lists/list.ind#1/1
-alias AllS_assoc /Coq/Lists/TheoryList/Lists/Assoc_sec/AllS_assoc.ind#1/1
-
-!A:Set.!B:Set.!P:!a:A.Prop.!l:(list (prod A B)).
- !H:(AllS_assoc A B P l).
-  (and
-   (eq (list (prod A B)) l l)
-   (eqT !n:A.Prop P P))
-
-(* Intros; Elim H:
-
-?1: (A,B:Set; P:(A->Prop); l:(list A*B))
-     (AllS_assoc A B P l) -> (nil A*B)=(nil A*B)/\P==P
-?2: (A,B:Set; P:(A->Prop); l:(list A*B))
-     (AllS_assoc A B P l) ->
-      (a:A; b:B; l0:(list A*B))
-       (P a) -> (AllS_assoc A B P l0) -> l0=l0/\P==P ->
-        (cons (a,b) l0)=(cons (a,b) l0)/\P==P
-[A,B:Set; P:(A->Prop); l:(list A*B); H:(AllS_assoc A B P l)]
- (AllS_assoc_ind A B P [l0:(list A*B)]l0=l0/\P==P
-  (?1 A B P l H) (?2 A B P l H) l H)
-
-*)