proposition: Lemma typing_normal_form {Gamma P t} : typing Gamma P t -> exists Q, normal_form Q /\ typing Gamma Q t.
proof: Proof. intros H. destruct (sn_normal _ _ _ H (SN H)) as (Q & H1 & H2). exists Q. split. eassumption. eapply preservation_star; eauto. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms