proposition: Lemma sn_normal_form Γ P s : typing Γ P s -> (forall Q, ~ step P Q) -> nf P.
proof: Proof. intros H Hstep. induction H; cbn in *. - eauto. - econstructor. destruct P. all: try now (eapply IHtyping1; intros ? ?; eapply Hstep; eauto). + exfalso. eapply Hstep; eauto. + inversion H. + eapply nf_normal_form, IHtyping2. intros ? ?; eapply Hstep; eauto. - eapply nf_normal_form, IHtyping. intros ? ?. eapply Hstep. eauto. - econstructor. destruct P. all: try now (eapply IHtyping; intros ? ?; eapply Hstep; eauto). + inversion H. + exfalso. eapply Hstep. eauto. - eapply nf_normal_form, IHtyping. intros ? ?. eapply Hstep. 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