first moogle template checkin

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

diff --git a/helm/gTopLevel/esempi/elim2.cic b/helm/gTopLevel/esempi/elim2.cic
index da77539661f9152f7dd894f06bbe12700b55d91f..b7c01b96ab3620e8dd285ab5ac7b63ff882f856a 100644 (file)
--- a/helm/gTopLevel/esempi/elim2.cic
+++ b/helm/gTopLevel/esempi/elim2.cic
@@ -1,6 +1,6 @@
 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 eq         /Coq/Init/Logic/eq.ind#1/1
+alias eq_ind     /Coq/Init/Logic/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
@@ -9,15 +9,18 @@ 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 and        /Coq/Init/Logic/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
+alias list       /Coq/Lists/PolyList/list.ind#1/1
+alias AllS_assoc /Coq/Lists/TheoryList/AllS_assoc.ind#1/1
+alias V          /Coq/Lists/PolyList/Lists/A.var
+alias VA         /Coq/Lists/TheoryList/Lists/A.var
+alias VB         /Coq/Lists/TheoryList/Lists/Assoc_sec/B.var
 
-!A:Set.!B:Set.!P:!a:A.Prop.!l:(list (prod A B)).
- !H:(AllS_assoc A B P l).
+!A:Set.!B:Set.!P:!a:A.Prop.!l:list{V := (prod A B)}.
+ !H:(AllS_assoc {VA := A ; VB := B} P l).
   (and
-   (eq (list (prod A B)) l l)
+   (eq list{V := (prod A B)} l l)
    (eqT !n:A.Prop P P))
 
 (* Intros; Elim H: