proposition: Theorem typing_to_pure_typing {Gamma P t} : typing Gamma P t -> pure_typing Gamma (erase P) t.
proof: Proof. elim => *. - by apply: pure_typing_pure_var_simpleI. - apply: pure_typing_pure_app_simpleI; by eassumption. - by apply: pure_typing_pure_abs_simpleI. - by apply: pure_typing_poly_absE. - by apply: (pure_typing_many_poly_absI (n := 1)). 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) ssreflect ssrbool ssrfun