proposition: Lemma ord_repeated n A: ord' (repeat A n) <= ord A.
proof: Proof. induction n; cbn; (eauto 2). lia. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)