X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Ftypes.ma;h=494177cfc11058555764c44e6a9a619e3fe0e27d;hb=cf367920b94b3a95c5c068c2f0672b97bf579731;hp=c14cc60b4bf4f32ef21f34965932982f2fafdc44;hpb=8f08fac33a366b2267b35af1a50ad3a9df8dbb88;p=helm.git

diff --git a/weblib/basics/types.ma b/weblib/basics/types.ma
index c14cc60b4..494177cfc 100644
--- a/weblib/basics/types.ma
+++ b/weblib/basics/types.ma
@@ -25,10 +25,10 @@ interpretation "Pair construction" 'pair x y = (pair ? ? x y).
 
 interpretation "Product" 'product x y = (Prod x y).
 
-definition fst ≝ λA,B.λp:A × B.
+definition fst ≝ λA,B.λp:A a title="Product" href="cic:/fakeuri.def(1)"×/a B.
   match p with [pair a b ⇒ a]. 
 
-definition snd ≝ λA,B.λp:A × B.
+definition snd ≝ λA,B.λp:A a title="Product" href="cic:/fakeuri.def(1)"×/a B.
   match p with [pair a b ⇒ b].
 
 interpretation "pair pi1" 'pi1 = (fst ? ?).
@@ -38,8 +38,8 @@ interpretation "pair pi2" 'pi2a x = (snd ? ? x).
 interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
 interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
 
-theorem eq_pair_fst_snd: ∀A,B.∀p:A × B.
-  p = 〈 \fst p, \snd p 〉.
+theorem eq_pair_fst_snd: ∀A,B.∀p:A a title="Product" href="cic:/fakeuri.def(1)"×/a B.
+  p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p, a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p 〉.
 #A #B #p (cases p) // qed.
 
 (* sum *)