proposition: Lemma retype_ctx_ord n Gamma: 1 <= n -> ord' (retype_ctx n Gamma) <= n.
proof: Proof. intros H; induction Gamma; cbn; eauto; unfold retype_ctx in *. rewrite IHGamma; destruct dec2; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)