From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 14 Sep 2005 08:04:32 +0000 (+0000)
Subject: Product, pair and projections.
X-Git-Tag: V_0_1_2_1~6
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d43bf5cc314729905d4b65d51f0c1a6438e091a5;p=helm.git

Product, pair and projections.
---

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.