proposition: Lemma app_eq_nil' (s t : string bool) : s = t++s -> t = nil.
proof: Proof. destruct t; trivial. intros H. exfalso. assert (H' : |s| = |(b :: t) ++ s|) by now rewrite H at 1. cbn in H'. rewrite app_length in 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