proposition: Lemma prod_dec_lb A B eq_A eq_B (A_lb : forall x y : A, x = y -> eq_A x y = true) (B_lb : forall x y : B, x = y -> eq_B x y = true) (x y : A * B) : x = y -> prod_beq eq_A eq_B x y = true.
proof: Proof. intro H; specialize (A_lb _ _ (f_equal fst H)); specialize (B_lb _ _ (f_equal snd H)). cbn in *; cbv [fst snd] in *. rewrite A_lb, B_lb; reflexivity. Defined.
imports: Coq.Classes.Morphisms