From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 Dec 2011 15:41:12 +0000 (+0000)
Subject: More stuff from CerCo to the standard library.
X-Git-Tag: make_still_working~2004
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=179aad29c98fcb78c8859e8a044e342b9259dd02;p=helm.git

More stuff from CerCo to the standard library.
---

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index 46cc5dd4b..1dcd79b7a 100644
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -214,3 +214,10 @@ lemma pair_destruct_2:
  ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
  #A #B #a #b *; /2/
 qed.
+
+lemma coerc_pair_sigma:
+ ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x).
+#A #B #P * #a #b #p % [@a | /2/]
+qed.
+coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x)
+≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)).