proposition: Lemma app_bound n (s t : string bool) : |t| <= n -> |s++t| <= n + |s|.
proof: Proof. intros H. rewrite app_length. lia. 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