proposition: Lemma option_eqb_spec A B : reflect (A = B) (option_eqb A B).
proof: Proof. Proof using spec. destruct A, B; try now econstructor. cbn. destruct (spec x x0); econstructor; congruence. Qed.
imports: Undecidability.L(Tactics.LTactics Datatypes.LBool Tactics.GenEncode) Undecidability.L(Functions.EqBool)