proposition: Lemma unification_retract_backward n (I: orduni n X): 1 <= n -> OU n Y (unification_retract I) -> OU n X I.
proof: Proof. intros Leq (Delta & sigma & T & EQ). pose (C := Consts (map sigma (nats (length Gamma₀)))). pose (f y := match find y C with | Some x => length Delta + x | None => 0 end). exists (Delta ++ target' (map (ctype Y) C)). exists (sigma >> subst_consts (re f)). split. - eapply re_typing; auto. intros ???. eapply weakening_ordertyping_app; auto. intros x y H1 H2. eapply Consts_consts with (S := map sigma (nats (| Gamma₀ |))) in H2; auto using in_map, lt_nats. unfold f, C. eapply find_in in H2 as [? H3]; rewrite H3. rewrite nth_error_app2; simplify; auto. unfold target'; erewrite map_map, map_nth_error; simplify; auto. now eapply find_Some. - unfold s₀, t₀ in EQ; cbn in EQ. now rewrite <-!subst_consts_inject_backwards, 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)