proposition: Lemma pure_typable_pure_app_0_Mω {n1 n2 s x t1 t2 Gamma} : leftmost_poly_var s = Some (n2 + x) -> pure_typable (many_poly_abs n1 (poly_arr (many_poly_abs n2 (poly_arr s t1)) t2) :: Gamma) (pure_app (pure_var 0) Mω) -> exists n, s = many_poly_abs n (poly_var (n + (n2 + x))).
proof: Proof. move=> H /pure_typableE [?] [?] [/pure_typingE'] [?] [[<-]]. move=> /contains_many_poly_absE [?] [?]. set σ := (fold_right _ _ _). rewrite subst_poly_type_many_poly_abs /=. set n := (_ - length _). case Hn: (n); last done. subst n. move=> [? ?]. subst => /pure_typing_Mω [?] [?] [?] [?] [?] [+] [?]. rewrite subst_poly_type_many_poly_abs /=. move=> /many_poly_abs_eqE' [?] [+ ?]. subst. have [n' [s' [?]]] := many_poly_absI s. subst. case Es': (s'); [ | | by move=> /=]. - subst => _. move: H. rewrite leftmost_poly_var_many_poly_abs /=. move=> [?]. subst => *. by eexists. - rewrite subst_poly_type_many_poly_abs /=. move=> _ /esym /many_poly_abs_eqE'' => /(_ ltac:(done)) [?] [?] ?. subst. move: H. rewrite ?leftmost_poly_var_many_poly_abs /= leftmost_poly_var_subst_poly_type. move=> ->. rewrite /= ?iter_up_poly_type_poly_type ?leftmost_poly_var_ren_poly_type. case: (leftmost_poly_var _); last done. move=> ? /= []. by lia. 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