proposition: Lemma listable_obstring n : listable (obstring n).
proof: Proof. destruct (listable_bstring n) as [L HL]. exists (None :: map Some L). intros [x|]. - right. apply in_map, HL. - cbn. eauto. Qed.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation