X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Ftypes.ma;h=efc213f95da759cb305ef3d1522ee13691de78e0;hb=dbc57c92512c04b3fd88f8289bb8dbe99b2f90e0;hp=b7a022ad201056d7d5d1842ea9b3def64d0d862b;hpb=464187875cc79b9ad2d415e638250fb949186670;p=helm.git

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index b7a022ad2..efc213f95 100644
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -9,6 +9,7 @@
      \ /   GNU General Public License Version 2   
       V_______________________________________________________________ *)
 
+include "basics/core_notation/pair_2.ma".
 include "basics/logic.ma".
 
 (* void *)
@@ -67,7 +68,7 @@ interpretation "mk_DPair" 'mk_DPair x y = (mk_DPair ?? x y).
 
 (* sigma *)
 record Sig (A:Type[0]) (f:A→Prop) : Type[0] ≝ {
-    pi1: A
+    pi1: A  (* not a coercion due to problems with Cerco *)
   ; pi2: f pi1
   }.
   
@@ -79,6 +80,9 @@ lemma sub_pi2 : ∀A.∀P,P':A → Prop. (∀x.P x → P' x) → ∀x:Σx:A.P x.
 #A #P #P' #H1 * #x #H2 @H1 @H2
 qed.
 
+lemma inj_mk_Sig: ∀A,P.∀x. x = mk_Sig A P (pi1 A P x) (pi2 A P x).
+#A #P #x cases x //
+qed-. 
 (* Prod *)
 
 record Prod (A,B:Type[0]) : Type[0] ≝ {