X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fesempi%2Felim2.cic;h=f44eba834838f412480b6d73b46bb3daa1b25263;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=b7c01b96ab3620e8dd285ab5ac7b63ff882f856a;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/gTopLevel/esempi/elim2.cic b/helm/gTopLevel/esempi/elim2.cic
index b7c01b96a..f44eba834 100644
--- 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))