proposition: Lemma eval_beta (M : model) s t ρ : eval M ρ (subst_poly_type (t .: poly_var) s) == eval (lift M) (eval M ρ t .: ρ >> Var M) s.
proof: Proof. rewrite eval_subst. 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