proposition: Lemma decompose_M_W : pure_typable Gamma_W M_W -> exists s, pure_typing Gamma_W N_W (poly_arr s s).
proof: Proof. move=> [?] /pure_typingE /= [?] [?] [?] [?] [+] [+] [_ ?]. move=> /pure_typingE' [?] [[?]]. subst. move=> /(contains_poly_arrE (n := 2)) [?] [?] [? ?]. subst. rewrite map_ren_poly_type_Gamma_W => ?. eexists. by eassumption. 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