-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).
+interpretation "First projection" 'fst x =
+ (cic:/matita/datatypes/constructors/fst.con _ _ x).
+
+notation "\fst x" with precedence 89
+for @{ 'fst $x}.
+
+interpretation "Second projection" 'snd x =
+ (cic:/matita/datatypes/constructors/snd.con _ _ x).
+
+notation "\snd x" with precedence 89
+for @{ 'snd $x}.
+
+theorem eq_pair_fst_snd: \forall A,B:Set.\forall p:Prod A B.
+p = 〈 (\fst p), (\snd p) 〉.