proposition: Lemma head_atom s: normal s -> ~ isLam s -> isAtom (head s).
proof: Proof. induction s; cbn; eauto. intros H _; cbn. eapply IHs1; eauto. destruct s1; eauto. intros _. eapply H; eauto. Qed.
imports: Undecidability.HOU(calculus.prelim calculus.terms calculus.syntax std.std) Morphisms Lia FinFun