proposition: Lemma ordertyping_one_atom Gamma (s: exp X) A: Gamma ⊢ s : A -> nf s -> ord A <= 1 -> isAtom (head s).
proof: Proof. destruct 2; subst; intros. destruct k; cbn; simplify; [eauto|]. inv H. now eapply ord_arr_one in H0. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)