proposition: Lemma ord'_rev L: ord' (rev L) = ord' L.
proof: Proof. induction L; cbn; rewrite ?ord'_app; trivial. simplify; cbn; trivial. rewrite IHL. simplify. eapply Nat.max_comm. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)