proposition: Lemma unification_monotone_forward n (I: orduni n X): OU n X I -> OU (S n) X (unification_monotone I).
proof: Proof. intros (Delta & sigma & T & H). exists Delta; exists sigma. intuition. eapply ordertypingSubst_monotone; eauto. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)