proposition: Lemma nf_normal_form P : nf P -> normal_form P.
proof: Proof. destruct P; cbn; eauto. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.typing_facts Undecidability.SystemF.Util.term_facts Coq.Relations.Relation_Operators Coq.Program.Equality