fact: Definition sum_eqb (A B : X + Y) := match A,B with | inl a,inl b => eqb__X a b | inr a,inr b => eqb__Y a b | _,_ => false end.
imports: Undecidability.L(Tactics.LTactics Datatypes.LBool) Undecidability.L(Tactics.GenEncode)