proposition: Theorem pure_typable_intro_poly_arr_0_0 M : { N | forall Gamma, pure_typable (map tidy ((poly_arr (poly_var 0) (poly_var 0)) :: (map (ren_poly_type S) Gamma))) M <-> pure_typable (map tidy Gamma) N }.
proof: Proof. exists (M_Wells_J M) => Gamma. constructor. - pose tI := poly_arr (poly_var 0) (poly_var 0). move=> HM. rewrite /M_Wells_J. pose t0 := poly_arr tI tI. exists t0. apply: (pure_typing_pure_app_simpleI (s := poly_abs t0)). + apply: pure_typing_pure_abs_simpleI. apply: pure_typing_K'I. * apply: (pure_typing_pure_app_simpleI (s := t0)). ** apply: (pure_typing_pure_var 0); [done | by apply /rt_step /contains_step_subst]. ** apply: (pure_typing_pure_var 0); [done | by apply /rt_step /contains_step_subst]. * pose s0 := poly_arr (poly_abs (poly_var 0)) (poly_abs (poly_var 0)). exists s0. apply: (pure_typing_pure_app_simpleI (s := s0)). ** apply: (pure_typing_pure_var 0); [done | by apply /rt_step /contains_step_subst]. ** apply: pure_typing_pure_abs_simpleI. apply: (pure_typing_pure_app_simpleI (s := (poly_abs (poly_var 0)))). *** apply: (pure_typing_pure_var 0); [done | by apply /rt_step /contains_step_subst]. *** apply: (pure_typing_pure_var 0); [done | by apply /rt_step /contains_step_subst]. + rewrite /M_Wells. apply: (pure_typing_pure_abs 1). apply: pure_typing_K'I; first by apply: pure_typing_pure_var_simpleI. apply: pure_typable_K'I. * exists tI. apply: pure_typing_pure_abs_simpleI. apply: pure_typing_pure_app_simpleI; first by apply: pure_typing_pure_var_simpleI. apply: pure_typing_pure_app_simpleI; by apply: pure_typing_pure_var_simpleI. * move: HM. rewrite /= ?map_map. congr pure_typable. congr cons. apply: map_ext => ?. by rewrite tidy_ren_poly_type. - rewrite /M_Wells_J. move=> /pure_typableE [s] [?] []. move=> /pure_typingE' /pure_typableI /pure_typable_K'E []. have [ns [s' [? Hs]]] := many_poly_absI s. subst s. rename s' into s. move=> /[dup] [H00] /pure_typable_self_application => /(_ _ _ ltac:(eassumption) ltac:(done)). move=> [y [Hyns Hsy]] H. rewrite /M_Wells. move=> /pure_typingE [nM] [?] [?] [+ /many_poly_abs_eqE']. case Es: (s); [by move=> + [] | | by subst s]. clear Hs => + [?] [? ?]. subst. move=> /pure_typing_K'E [] /pure_typingE [?] [?] [?] [[?]] [H1c ?]. subst. move=> /pure_typable_K'E [/pure_typableE] [?] /pure_typableE [?] [?] []. move=> /pure_typingE' [?] [[?]] H2c. subst. move=> /pure_typingE [?] [?] [?] [?] [+] [_] [H3c ?]. subst. move=> /pure_typingE' [?] [[?]] H4c HM. subst. move: (Hsy) => /= /leftmost_poly_var_contains_poly_arr => /(_ _ _ ltac:(eassumption)). move=> [?] [?] [?] ?. subst. move: Hsy. rewrite /= leftmost_poly_var_many_poly_abs /=. move: H => /pure_typable_pure_app_0_Mω H /H{H} [? ?]. subst. move: H2c => /contains_poly_arrE [?] [?] [+ ?]. subst. rewrite subst_poly_type_many_poly_abs /= iter_up_poly_type_poly_type. rewrite fold_right_length_ts ?iter_up_poly_type_poly_type /=. move=> /many_poly_abs_eqE'' => /(_ ltac:(done)) [?] [? ?]. subst. move: H4c. rewrite ren_poly_type_many_poly_abs /=. move=> /contains_poly_arrE [?] [?] [? ?]. subst. move: (H3c) => /contains_tidyI. rewrite tidy_many_poly_abs_le /=; first by lia. move=> /contains_poly_varE [?] [?]. set t := (t in ren_poly_type _ t). have [nt' [t' [?]]] := many_poly_absI t. subst t. subst. case Et': (t'); [move=> _ | move=> _ | by subst t'; move=> /= ]. + subst t'. move: (H1c). rewrite ren_poly_type_many_poly_abs /=. move=> /contains_sub [?] [?] [?] [?] _. subst. move: H00. rewrite many_poly_abs_many_poly_abs. move=> /pure_typable_pure_app_0_0' [y' ?] _. subst. move: H3c => /contains_tidyI. rewrite tidy_many_poly_abs_le /=; first by lia. rewrite tidy_subst_poly_type tidy_ren_poly_type tidy_many_poly_abs_le /=; first by lia. rewrite iter_up_ren_ge; first by lia. rewrite fold_right_length_ts_ge /=; first by lia. move=> /containsE [?]. have ? : y = y' by lia. subst. move: HM => [?] /pure_typing_tidyI /=. rewrite tidy_many_poly_abs_le /=. { rewrite ?allfv_poly_type_many_poly_abs /= ?iter_scons_ge; by lia. } rewrite tidy_many_poly_abs_le /=; first by lia. rewrite tidy_many_poly_abs_le /=; first by lia. move=> /(pure_typing_ren_poly_type (fun x => x - (nM - 1))) /= /pure_typableI. congr pure_typable. congr cons. * congr poly_arr; congr poly_var; by lia. * rewrite ?map_map. apply: map_ext => ?. rewrite ?tidy_ren_poly_type tidy_tidy ?poly_type_norm /=. apply: extRen_poly_type. by lia. + rewrite ren_poly_type_many_poly_abs subst_poly_type_many_poly_abs /=. rewrite (svalP tidy_many_poly_abs). by move: (sval _) => [? ?] /many_poly_abs_eqE' /= []. 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