proposition: Lemma retype_type_ord n A: 1 <= n -> ord (retype_type n A) <= S n.
proof: Proof. intros H; induction A; cbn [retype_type]. - cbn; lia. - destruct dec2; simplify; intuition (auto with arith). Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)