New definition of finset.

[helm.git] / matita / matita / lib / basics / types.ma

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index b7a022ad201056d7d5d1842ea9b3def64d0d862b..94777e0710e6c28e230c1e407426c1b62ce3e8b6 100644 (file)
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -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] ≝ {