proposition: Lemma pure_typable_M_W : typing Gamma_W P_W (poly_var 0) -> pure_typable Gamma_W M_W.
proof: Proof. move=> /typing_to_pure_typing /pure_typableI. by rewrite erase_P_W. 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