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 b7c01b96ab3620e8dd285ab5ac7b63ff882f856a..f44eba834838f412480b6d73b46bb3daa1b25263 100644 (file)
--- a/helm/gTopLevel/esempi/elim2.cic
+++ b/helm/gTopLevel/esempi/elim2.cic
@@ -23,6 +23,11 @@ alias VB         /Coq/Lists/TheoryList/Lists/Assoc_sec/B.var
    (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))