proposition: Lemma E_tlam s ρ P : sn P -> (forall ξ p t, E s (p .: ρ) (subst_term (t .: ξ >> poly_var) var P)) -> E (poly_abs s) ρ (ty_abs P).
proof: Proof. induction 1 as [P _ IH]. intros H. econstructor. - rewrite K_all. intros _. eapply H. - intros Q Hst. inv Hst. eapply IH. eauto. intros ξ p t. eapply R_step; eauto using step_subst. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms