list.ma moved inside lists.

[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 c14cc60b4bf4f32ef21f34965932982f2fafdc44..f35dde531e5fe93debc3f5b0e54ebb78c8f9425b 100644 (file)
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -42,6 +42,12 @@ theorem eq_pair_fst_snd: ∀A,B.∀p:A × B.
   p = 〈 \fst p, \snd p 〉.
 #A #B #p (cases p) // qed.
 
+lemma fst_eq : ∀A,B.∀a:A.∀b:B. \fst 〈a,b〉 = a.
+// qed.
+
+lemma snd_eq : ∀A,B.∀a:A.∀b:B. \snd 〈a,b〉 = b.
+// qed.
+
 (* sum *)
 inductive Sum (A,B:Type[0]) : Type[0] ≝
   inl : A → Sum A B
@@ -56,4 +62,6 @@ inductive option (A:Type[0]) : Type[0] ≝
 
 (* sigma *)
 inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝
-  dp: ∀a:A.(f a)→Sig A f.
\ No newline at end of file
+  dp: ∀a:A.(f a)→Sig A f.
+  
+interpretation "Sigma" 'sigma x = (Sig ? x).