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