proposition: Lemma retype_iff n (I: orduni n X): 1 <= n -> OU n X I <-> OU n X (@retype n I).
proof: Proof. intros Leq. rewrite orduni_normalise_correct. destruct I as [Gamma s t A ? ?]; unfold orduni_normalise, retype, OU; cbn. split; intros (Delta & sigma & ? & ?); eapply conservativity.ordertyping_weak_ordertyping. 1,3,4,6:now eauto. all: intros ??; simplify; intros ? [H'|H']; eapply H. all: rewrite nth_error_map_option in *. all: destruct (nth Gamma x) eqn: N; try discriminate; cbn in *. all: destruct dec2 as [|L]; eauto. all: exfalso; eapply L. all: eauto using vars_ordertyping_nth, eta₀_typing. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)