X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Ftypes.ma;h=1dcd79b7a49892702ba1290f86f3cb0099d3e335;hb=927bda3b4b7fe5f521ae73eb008a746e8606a0b4;hp=1d38830481c02fa51a4121918f8941fbeaee8285;hpb=dc35589f8448d6a7bd803992e918acc7b720e7fb;p=helm.git

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index 1d3883048..1dcd79b7a 100644
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -57,16 +57,13 @@ 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
   }.
 
-interpretation "DPair" 'sigma x = (DPair ? x).
+interpretation "DPair" 'dpair x = (DPair ? x).
 
-notation "hvbox(« term 19 a, break term 19 b»)" 
-with precedence 90 for @{ 'dp $a $b }.
-
-interpretation "mk_DPair" 'dp x y = (mk_DPair ?? x y).
+interpretation "mk_DPair" 'mk_DPair x y = (mk_DPair ?? x y).
 
 (* sigma *)
 record Sig (A:Type[0]) (f:A→Prop) : Type[0] ≝ {
@@ -78,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] ≝ {
@@ -213,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 ??)).