+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.
+