proposition: Lemma pure_typing_fold_right_many_pure_app {Gamma x s' nss t M} : nth_error Gamma x = Some (fold_right (fun '(n, s) r => many_poly_abs n (poly_arr s r)) s' nss) -> pure_typing Gamma (many_pure_app (pure_var x) (repeat M (length nss))) t -> exists ns' ξ' nt' t', t = many_poly_abs nt' t' /\ contains (many_poly_abs ns' (ren_poly_type ξ' s')) t'.
proof: Proof. rewrite -[Gamma in pure_typing Gamma _ _]map_ren_poly_type_id. move: (id) => ξ. elim /rev_ind: nss Gamma ξ s' t. - move=> Gamma ξ > Hx /= /pure_typingE [n1] [?] [?]. rewrite ?map_map nth_error_map Hx => [[[<-]]]. rewrite poly_type_norm /= => [[HC ->]]. exists 0. do 3 eexists. constructor; [by reflexivity | by eassumption]. - move=> [n s] nss IH /= Gamma ξ s' t. rewrite fold_right_app /= => /IH {}IH. rewrite app_length repeat_app many_pure_app_app /=. move=> /pure_typingE [n1] [?] [?] [?] [+] [_] [H1C ?]. subst. rewrite ?map_map. under map_ext => ? do rewrite poly_type_norm. move=> /IH [n1s'] [n2s'] [nt'] [t'] []. case: nt'; last done. move=> /= ?. subst. rewrite ren_poly_type_many_poly_abs many_poly_abs_many_poly_abs /=. move=> /contains_poly_arrE [?] [?] [? ?]. subst. move: H1C => /contains_subst_poly_type_fold_rightE. clear=> ?. do 4 eexists. constructor; [by reflexivity | by eassumption]. 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