proposition: Lemma sum_eqb_spec A B : reflect (A = B) (sum_eqb A B).
proof: Proof. Proof using spec__X spec__Y. destruct A, B; (try now econstructor);cbn. - destruct (spec__X x x0); econstructor;congruence. - destruct (spec__Y y y0); constructor;congruence. Qed.
imports: Undecidability.L(Tactics.LTactics Datatypes.LBool) Undecidability.L(Tactics.GenEncode)