proposition: Lemma order_one_lambda_free Gamma s A: normal s -> (Gamma ⊢(1) s : A) -> isAtom (head s) -> lambda_free s.
proof: Proof. intros N % normal_nf. induction N in Gamma, A |-*; subst. destruct k; cbn;[intros|easy]. simplify in H1. eapply lambda_free_AppR. - destruct s; cbn in i; intuition econstructor. - eapply AppR_ordertyping_inv in H0 as H4; destruct H4 as [L H4]. intuition idtac. assert (ord' L <= 1). + destruct s; cbn in i. 3-4:easy. * inv H3. simplify in H6. lia. * inv H3. rewrite H6 in H7. simplify in H7. lia. + eapply orderlisttyping_element in H2 as [B []]. 2:now eauto. eapply H; [eauto..|]. eapply ordertyping_one_atom; [eauto..|]. eapply ord'_elements; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)