proposition: Lemma pure_typing_Mω {Gamma t} : pure_typing Gamma Mω t -> exists n1 n2 s' t' y, t = many_poly_abs n1 (poly_arr (many_poly_abs n2 s') t') /\ y < n2 /\ leftmost_poly_var s' = Some y.
proof: Proof. rewrite /Mω. move=> /pure_typingE [n1] [s] [t'] [+ ->]. have := many_poly_absI s. move=> [n] [s'] [->]. move=> + /pure_typableI /pure_typable_self_application. move=> + H => /H /= => /(_ _ ltac:(done)) [y] [? ?]. by exists n1, n, s', t', y. Qed.
imports: List Lia Relation_Definitions Relation_Operators Operators_Properties Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts term_facts typing_facts iipc2_facts pure_typing_facts) ssreflect ssrbool ssrfun