proposition: Lemma E_tapp s t ρ P r : E (poly_abs s) ρ P -> E (subst_poly_type (t .: poly_var) s) ρ (ty_app P r).
proof: Proof. induction 1 as [P H IH H2]. eapply E_beta. econstructor. inversion 1. intros Q Hst. inv Hst. - specialize (H eq_refl). rewrite K_all in H. eauto. - eapply H2 in H4. now eapply E_beta in H4. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms