proposition: Lemma app_neq b (s t : string bool) : s <> (b :: t) ++ s.
proof: Proof. intros H. apply app_eq_nil' in H. discriminate. 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