proposition: Theorem typing_to_type_assignment {Gamma P t} : typing Gamma P t -> type_assignment Gamma (erase P) t.
proof: Proof. elim. - move=> *. by apply: type_assignment_var. - move=> * /=. apply: type_assignment_app; by eassumption. - move=> * /=. by apply: type_assignment_abs. - move=> * /=. by apply: type_assignment_inst. - move=> * /=. by apply: type_assignment_gen. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts term_facts) ssreflect ssrbool ssrfun