proposition: Lemma normal_nf s: normal s -> nf s.
proof: Proof. induction s. + intros. exists 0 (var f) nil; cbn; intuition. + intros. exists 0 (const c) nil; cbn; intuition. + intros H; mp IHs; eauto using normal_lam_elim; destruct IHs as [k s' t' T H1]. exists (S k) s' T; (eauto 1); cbn; congruence. + intros H; eapply normal_app_r in H as Ns1; eapply normal_app_l in H as Ns2. mp IHs1; (eauto 1); mp IHs2; (eauto 2). destruct IHs1. subst t. destruct k; [|exfalso; eapply H; cbn; eauto]. exists 0 s (s2 :: T); (eauto 1); cbn; simplify. intros t. destruct (s2 == t); subst; intuition. destruct (t el T); intuition. exfalso; intuition. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)