Added examples.

[helm.git] / helm / gTopLevel / esempi / elim2.cic

diff --git a/helm/gTopLevel/esempi/elim2.cic b/helm/gTopLevel/esempi/elim2.cic
new file mode 100644 (file)
index 0000000..da77539
--- /dev/null
+++ b/helm/gTopLevel/esempi/elim2.cic
@@ -0,0 +1,36 @@
+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)
+
+*)