Product, pair and projections.

diff --git a/helm/matita/library/datatypes/constructors.ma b/helm/matita/library/datatypes/constructors.ma
index c2bdc566b9034e333a9d9bd869d8966600e880e5..2ac1cb376804ad8e89dbd2a805cbd9c1c1284065 100644 (file)
--- a/helm/matita/library/datatypes/constructors.ma
+++ b/helm/matita/library/datatypes/constructors.ma
@@ -13,12 +13,26 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/datatypes/constructors/".
+include "logic/equality.ma".
 
 inductive void : Set \def.
 
 inductive Prod (A,B:Set) : Set \def
 pair : A \to B \to Prod A B.
 
+definition fst \def \lambda A,B:Set.\lambda p: Prod A B.
+match p with
+[(pair a b) \Rightarrow a]. 
+
+definition snd \def \lambda A,B:Set.\lambda p: Prod A B.
+match p with
+[(pair a b) \Rightarrow b].
+
+theorem eq_pair_fst_snd: \forall A,B:Set.\forall p: Prod A B.
+p = pair A B (fst A B p) (snd A B p).
+intros.elim p.simplify.reflexivity.
+qed.
+
 inductive Sum (A,B:Set) : Set \def
   inl : A \to Sum A B
-| inr : B \to Sum A B.
\ No newline at end of file
+| inr : B \to Sum A B.