proposition: Lemma iprep_respectful s t t' : t == t' -> iprep s t == iprep s t'.
proof: Proof. Proof using HER1. intros Ht. induction s. - cbn. easy. - cbn. apply HER1. easy. 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