proposition: Lemma is_rep_subst s t x y sigma : (is_rep (comb_rel s t) x y)[sigma] = is_rep (comb_rel s t) x`[sigma] y`[sigma].
proof: Proof. unfold is_rep. cbn -[comb_rel]. subsimpl. repeat f_equal. - unfold comb_rel. cbn. rewrite !prep_string_subst. reflexivity. - unfold comb_rel. cbn. rewrite !prep_string_subst. reflexivity. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullFacts Undecidability.FOL.Deduction.FullNDFacts Undecidability.FOL.Sets.FST Undecidability.FOL.FST Undecidability.FOL.Reductions.PCPb_to_FST Undecidability.PCP(PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb) Undecidability(Shared.ListAutomation)