proposition: Lemma ienc_iprep s t : iprep s (ienc t) == ienc (s ++ t).
proof: Proof. Proof using HER1 HE3 HE1. induction s; cbn; trivial. apply HER1. apply (HE3 IHs). apply HE1. 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