ocaml 3.09 transition

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

diff --git a/helm/gTopLevel/esempi/elim2.cic b/helm/gTopLevel/esempi/elim2.cic
index da77539661f9152f7dd894f06bbe12700b55d91f..f44eba834838f412480b6d73b46bb3daa1b25263 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,17 +9,25 @@ 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))
 
+\forall A,B: Set. \forall P: A \to Prop.
+ \forall l: list \subst [ A \Assign (prod A B) ].
+  \forall H:(AllS_assoc \subst [ A \Assign A ; B \Assign B] P l).
+    l = l \wedge P = P
+
 (* Intros; Elim H:
 
 ?1: (A,B:Set; P:(A->Prop); l:(list A*B))