proposition: Lemma order_head Gamma s A B: Gamma ⊢ s : A -> Gamma ⊢ (head s) : B -> isAtom (head s) -> ord A <= ord B.
proof: Proof. induction 1; trivial; cbn. - intros H1 _; inv H1. rewrite H in H2; injection H2 as ->; eauto. - intros H1; inv H1; eauto. - easy. - intros; rewrite <-IHtyping1; trivial. rewrite ord_arr; eauto. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)