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