proposition: Lemma typing_P_W : typing Gamma_W Q_W (poly_arr t_x_W t_x_W) -> typing Gamma_W P_W (poly_var 0).
proof: Proof. rewrite /P_W. apply: typing_app. apply: typing_ty_appI; [apply: typing_ty_appI |]; [by apply: typing_var | done | done]. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts term_facts typing_facts pure_typing_facts pure_typable_prenex) ssreflect ssrbool ssrfun