proposition: Lemma E_lam s t s' ρ P : sn P -> (forall ξ1 ξ2 Q, E s ρ Q -> E t ρ (subst_term (ξ1 >> poly_var) (Q .: ξ2 >> var) P)) -> E (poly_arr s t) ρ (abs s' P).
proof: Proof. induction 1 as [P _ IH]. intros H. econstructor. - intros _. rewrite K_arr. eauto. - intros Q Hst. inv Hst. eapply IH; eauto. intros. 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