proposition: Lemma pure_typable_many_pure_term_abs_allI M {Gamma} : pure_typable Gamma M -> pure_typable [] (many_pure_term_abs (pure_var_bound M) M).
proof: Proof. have := pure_var_boundP M. move: (pure_var_bound M) => n. elim: Gamma n M. - elim; first done. move=> n IH M HnM [tM]. move=> /(pure_typing_ren_pure_term id (Delta := [poly_var 0])). apply: unnest; first by case. rewrite ren_pure_term_id. move=> /(pure_typing_pure_abs 0 (Gamma := [])) /pure_typableI /IH. rewrite /many_pure_term_abs (ltac:(lia) : S n = n + 1) -iter_plus. apply. move=> /=. apply: allfv_pure_term_impl HnM. case; first done. move=> /=. by lia. - move=> s Gamma IH [|n] M. + move=> HM [tM]. move=> /(pure_typing_ren_pure_term_allfv_pure_term id (Delta := [])). rewrite ren_pure_term_id. apply: unnest; first by apply: allfv_pure_term_impl HM; lia. by move=> /pure_typableI. + move=> HnM [tM]. rewrite -[Gamma]map_ren_poly_type_id. move=> /(pure_typing_pure_abs 0) /pure_typableI /IH. rewrite /many_pure_term_abs (ltac:(lia) : S n = n + 1) -iter_plus. apply. move=> /=. apply: allfv_pure_term_impl HnM. case; first 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) ssreflect ssrbool ssrfun