proposition: Lemma eval_ren ξ s ρ : eval ρ (ren_poly_type ξ s) == eval (ξ >> ρ) s.
proof: Proof. induction s in ξ, ρ |- *; cbn. - reflexivity. - now rewrite IHs1, IHs2. - eapply All_ext. intros d. rewrite IHs. eapply eval_ext. now intros []. reflexivity. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms