proposition: Lemma prod_eqb_spec f g: (forall (x1 x2 : X) , reflect (x1 = x2) (f x1 x2)) -> (forall (y1 y2 : Y) , reflect (y1 = y2) (g y1 y2)) -> forall x y, reflect (x=y) (prod_eqb f g x y).
proof: Proof. Proof with try (constructor;congruence). intros Hf Hg [x1 y1] [x2 y2]. specialize (Hf x1 x2); specialize (Hg y1 y2);cbn. inv Hf;inv Hg;cbn... Qed.
imports: Undecidability.L.Datatypes(LBool) Undecidability.L(Functions.EqBool GenEncode)