From bc2a1fce21a66af077172344854c709b64b7fe82 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 18 Jun 2004 11:22:13 +0000
Subject: [PATCH] New syntax.

---
 helm/gTopLevel/esempi/elim2.cic | 5 +++++
 1 file changed, 5 insertions(+)

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))
-- 
2.39.2