fact: Definition bstring_step n (L : list (bstring n)) := [bnil (S n)] ++ map (bcons true) L ++ map (bcons false) L.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation