proposition: Theorem pure_typable_intro_poly_var_0 M : { N | forall Gamma, pure_typable (map tidy (poly_var 0 :: poly_arr (poly_var 0) (poly_var 0) :: (map (ren_poly_type S) Gamma))) M <-> pure_typable (map tidy Gamma) N }.
proof: Proof. pose N := pure_app (ren_pure_term S (pure_abs M)) (pure_app (pure_var 1) (pure_var 0)). have [N' HN'] := pure_typable_intro_poly_bot N. have [N'' HN''] := pure_typable_intro_poly_arr_0_0 N'. exists N'' => Gamma. constructor. - move=> [tM] HtM. apply /HN'' /HN' {HN'' HN'}. eexists. apply: (pure_typing_pure_app_simpleI (s := poly_var 0)). + move=> /=. apply: pure_typing_pure_abs_simpleI. apply: pure_typing_ren_pure_term; first by eassumption. by case. + apply: (pure_typing_pure_app_simpleI (s := poly_var 0)). * by apply: pure_typing_pure_var_simpleI. * apply: (pure_typing_pure_var 0); first by reflexivity. by apply /rt_step /(contains_step_subst (s := poly_var 0)). - move /HN'' /HN' {HN'' HN'}. rewrite /N. move=> /pure_typableE [?] [?] [] /= /pure_typingE' HM. move=> /pure_typingE [n3] [?] [?] [?] [+] [+] [H2C ?]. subst. move=> /pure_typingE' [?] [[?]] H3C _. subst. move: H3C => /containsE [H1E ?]. subst. move: H2C => /containsE ?. subst. move: HM => /=. set s := (s in pure_typing (s :: _) _ _). set Gamma' := (Gamma' in pure_typing (s :: _ :: Gamma') _ _). move=> /(pure_typing_ren_pure_term_allfv_pure_term (scons 0 (scons 1 S)) (Delta := s :: Gamma')). apply: unnest. { rewrite allfv_pure_term_ren_pure_term /=. apply: allfv_pure_term_TrueI. by case. } rewrite renRen_pure_term /= ren_pure_term_id'; first by case. subst s Gamma'. move=> /pure_typing_tidyI /=. rewrite tidy_many_poly_abs_le /=; first by lia. move=> /pure_typableI. congr pure_typable. congr cons; last congr cons. + congr poly_var. by lia. + rewrite ?map_map. apply: map_ext => ?. by rewrite tidy_tidy. 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