proposition: Lemma string_nil (s : string bool) : |s| <= 0 <-> s = nil.
proof: Proof. destruct s; cbn. - split; trivial; lia. - split; try congruence. intros H. 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