proposition: Lemma listable_bstring n : listable (bstring n).
proof: Proof. induction n. - exists [bnil 0]. intros [s H]. assert (s = nil) as -> by now apply string_nil. left. now apply bstring_eq. - destruct IHn as [L HL]. exists (bstring_step L). intros [ [|[] s] H]; apply in_app_iff; cbn in H. + left. left. now apply bstring_eq. + right. apply in_app_iff. left. apply in_map_iff. assert (H' : |s| <= n) by lia. exists (bcast H'). split; trivial. now apply bstring_eq. + right. apply in_app_iff. right. apply in_map_iff. assert (H' : |s| <= n) by lia. exists (bcast H'). split; trivial. now apply bstring_eq. 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