proposition: Lemma unification_retract_forward n (I: orduni n X): OU n X I -> OU n Y (unification_retract I).
proof: Proof. intros (Delta & sigma & T & EQ). exists Delta. exists (sigma >> subst_consts inj). split. - now eapply inj_typing. - unfold s₀, t₀; cbn. rewrite <-!subst_consts_inject_forward. now rewrite EQ. Qed.
imports: List Arith Lia Morphisms Setoid Undecidability.HOU(calculus.calculus) Undecidability.HOU(unification.higher_order_unification unification.nth_order_unification concon.conservativity_constants concon.conservativity)