X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Ftypes.ma;h=a5e35c9d218a5d756319dd429dd7e1b6d4e8363e;hb=53f874fba5b9c39a788085515a4fefe5d29281da;hp=35d5cd07b10b37df64cf2c4989c4ed0ae6d699de;hpb=bc477154d15f6979c948f9af602199af547d193e;p=helm.git

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index 35d5cd07b..a5e35c9d2 100644
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -47,7 +47,7 @@ lemma option_map_some : ∀A,B,f,x,v.
 definition option_map_def : ∀A,B:Type[0]. (A → B) → B → option A → B ≝
 λA,B,f,d,o. match o with [ None ⇒ d | Some a ⇒ f a ].
 
-lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → ⊥.
+lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → False.
   (∀v. x = Some ? v → Q (P v)) →
   Q (match x return λy.x = y → ? with [ Some v ⇒ λ_. P v | None ⇒ λE. match H E in False with [ ] ] (refl ? x)).
 #A #B #P #Q *
@@ -67,7 +67,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 +79,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] ≝ {