proposition: Lemma prod_dec_bl A B eq_A eq_B (A_bl : forall x y : A, eq_A x y = true -> x = y) (B_bl : forall x y : B, eq_B x y = true -> x = y) (x y : A * B) : prod_beq eq_A eq_B x y = true -> x = y.
proof: Proof. destruct x as [a b], y as [a' b']. specialize (A_bl a a'); specialize (B_bl b b'). cbn; intro H; destruct A_bl; [ | destruct B_bl; [ | reflexivity ] ]; edestruct eq_A; edestruct eq_B; cbn in *; try reflexivity; try assumption. Defined.
imports: Coq.Classes.Morphisms