proposition: Lemma ord_arr_one A B: ~ ord (A → B) <= 1.
proof: Proof. intros H; rewrite ord_arr in H; eapply Nat.max_lub_l in H. rewrite ord_1 with (A := A) in H; lia. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)