proposition: Lemma pair_equal_spec (A B : Type) (a1 a2 : A) (b1 b2 : B) : (a1, b1) = (a2, b2) <-> a1 = a2 /\ b1 = b2.
proof: Proof. Proof with auto. split; intro H. - split. + replace a1 with (fst (a1, b1)); replace a2 with (fst (a2, b2))... rewrite H... + replace b1 with (snd (a1, b1)); replace b2 with (snd (a2, b2))... rewrite H... - destruct H; subst... Qed.
imports: Notations Ltac Logic