fact: Definition option_eqb (A B : option X) := match A,B with | None,None => true | Some x, Some y => eqb x y | _,_ => false end.
imports: Undecidability.L(Tactics.LTactics Datatypes.LBool Tactics.GenEncode) Undecidability.L(Functions.EqBool)