X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fdatatypes%2Fconstructors.ma;h=2ac1cb376804ad8e89dbd2a805cbd9c1c1284065;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=c2bdc566b9034e333a9d9bd869d8966600e880e5;hpb=be797cb755104e7c8709f2602ced5c46c5c1987b;p=helm.git

diff --git a/helm/matita/library/datatypes/constructors.ma b/helm/matita/library/datatypes/constructors.ma
index c2bdc566b..2ac1cb376 100644
--- 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.