proposition: Lemma OU_NOU n I: 1 <= n -> OU n X I <-> NOU n I.
proof: Proof. intros Leq; split; intros (Delta & sigma & H1 & H2); [| exists Delta; exists sigma; intuition]. eapply ordertyping_normalise_subst in H1 as (tau & H5 & H6 & H7). pose (theta x := if nth (Gamma₀ I) x then tau x else var x). exists Delta. exists theta. intuition idtac. + intros ???; unfold theta; rewrite H; eapply H7; eauto. + rewrite subst_pointwise_equiv with (sigma := theta) (tau := sigma). rewrite subst_pointwise_equiv with (sigma := theta) (tau := sigma); trivial. all: intros ? H; eapply typing_variables in H; [|eauto]; domin H. all: unfold theta; now rewrite H, H5. + unfold theta; destruct nth eqn: ?; [|eauto]; domin Heqo; eauto. Qed.
imports: List Lia Morphisms Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification unification.systemunification)