From 910b8e95135bfabb852c2e6d918ff50bdcb98d0a Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 Dec 2011 14:39:09 +0000
Subject: [PATCH] Some more lemmas from CerCo.

---
 matita/matita/lib/basics/types.ma | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index d093202b1..46cc5dd4b 100644
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -57,7 +57,7 @@ lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. 
 
 (* dependent pair *)
 record DPair (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ {
-    dpi1: A
+    dpi1:> A
   ; dpi2: f dpi1
   }.
 
@@ -75,6 +75,10 @@ interpretation "Sigma" 'sigma x = (Sig ? x).
 
 interpretation "mk_Sig" 'dp x y = (mk_Sig ?? x y).
 
+lemma sub_pi2 : ∀A.∀P,P':A → Prop. (∀x.P x → P' x) → ∀x:Σx:A.P x. P' (pi1 … x).
+#A #P #P' #H1 * #x #H2 @H1 @H2
+qed.
+
 (* Prod *)
 
 record Prod (A,B:Type[0]) : Type[0] ≝ {
-- 
2.39.2