proposition: Lemma pure_typable_many_pure_app_repeat_poly_var {Gamma x y ny nss t} : nth_error Gamma x = Some (fold_right (fun '(n, s) r => many_poly_abs n (poly_arr s r)) t nss) -> nth_error Gamma y = Some (poly_var ny) -> pure_typable Gamma (many_pure_app (pure_var x) (repeat (pure_var y) (length nss))) -> Forall (fun '(_, s) => exists n x, s = many_poly_abs n (poly_var (n + x))) nss.
proof: Proof. move=> + Hy. elim /rev_ind: nss t; first done. move=> [n s] nss IH t. rewrite fold_right_app /= => Hx. rewrite app_length repeat_app many_pure_app_app /=. move=> /pure_typableE [?] [?] []. move=> /[dup] [/pure_typableI /IH] /(_ _ Hx) Hnss. move=> /(pure_typing_fold_right_many_pure_app Hx) [?] [?] [[|?]] [?] []; last done. move=> /= ?. subst. rewrite ren_poly_type_many_poly_abs many_poly_abs_many_poly_abs /=. move=> /contains_poly_arrE [?] [?] [? ?]. subst. move=> /pure_typingE [?] [?] [?] [+] [+]. rewrite nth_error_map Hy => [[?]]. subst. rewrite poly_type_norm. move=> /containsE <-. move=> /esym /many_poly_abs_poly_var_eq_subst_poly_typeE [?] [?] [?] [? ->]. apply /Forall_app. constructor; first done. constructor; last done. clear. by do 2 eexists. 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