proposition: Theorem pure_typable_intro_poly_bot M : { N | forall Gamma, pure_typable (map tidy ((poly_abs (poly_var 0)) :: Gamma)) M <-> pure_typable (map tidy Gamma) N }.
proof: Proof. exists (pure_abs M) => Gamma. constructor. - by move=> [tM] /= /pure_typing_pure_abs_simpleI /pure_typableI. - move=> /pure_typableE [s] [t] HM /=. exists t. apply: (pure_typing_weaken_closed (s' := s) (Gamma1 := [])); [done | | done]. apply: (pure_typing_pure_var 0); [done | by apply /rt_step /contains_step_subst]. 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