proposition: Lemma E_beta s t ρ : E (subst_poly_type (t .: poly_var) s) ρ == E s (V t ρ .: ρ).
proof: Proof. intros P. now rewrite eval_beta. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms