proposition: Lemma K_arr s t ρ u P : K (poly_arr s t) ρ (abs u P) <-> forall ξ1 ξ2 Q, E s ρ Q -> E t ρ (subst_term (ξ1 >> poly_var) (Q .: ξ2 >> var) P).
proof: Proof. unfold M. cbn. pw. asimpl. eapply R_ext. reflexivity. now_asimpl. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms