proposition: Lemma K_all s ρ P : K (poly_abs s) ρ (ty_abs P) <-> forall ξ p t, E s (p .: ρ) (subst_term (t .: ξ >> poly_var) var P).
proof: Proof. unfold M. split. - intros H ξ p t. specialize (H ξ id p t). fold ren_term in H. eapply R_ext. 3:eapply H. reflexivity. now_asimpl. - intros H ξ1 ξ2 p t. specialize (H ξ1 p t). pose proof (Hren := R_ren id ξ2 _ _ H). asimpl in Hren. eapply R_ext. 3:eapply Hren. 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