proposition: Lemma injective_projections (A B:Type) (p1 p2:A * B) : fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2.
proof: Proof. destruct p1; destruct p2; simpl; intros Hfst Hsnd. rewrite Hfst; rewrite Hsnd; reflexivity. Qed.
imports: Notations Ltac Logic