proposition: Theorem typing_of_type_assignment {Gamma M t} : type_assignment Gamma M t -> exists P, M = erase P /\ typing Gamma P t.
proof: Proof. elim. - move=> ? x ? ?. exists (var x). constructor; [done | by apply: typing_var]. - move=> > ? [P [? ?]] ? [Q [? ?]]. exists (app P Q). subst. constructor; [done | by apply: typing_app; eassumption]. - move=> ? ? s ? ? [P [? ?]]. exists (abs s P). subst. constructor; [done | by apply: typing_abs]. - move=> ? ? ? {}t ? [P [? ?]]. exists (ty_app P t). subst. constructor; [done | by apply: typing_ty_app]. - move=> > ? [P [? ?]]. exists (ty_abs P). subst. constructor; [done | by apply: typing_ty_abs]. 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