proposition: Lemma pair_2 : forall (A B : Type) (H1 H2 : A * B), fst H1 = fst H2 -> snd H1 = snd H2 -> H1 = H2.
proof: Proof. intros A B H1 H2. case H1. case H2. simpl in |- *. intros. rewrite H. rewrite H0. reflexivity. Qed.
imports: Coq(Lia)