proposition: Lemma remove_constants_backward n (I: orduni n X) (H: ord' (map (ctype X) (iConsts I)) < n): OU n Y (remove_constants n I H) -> OU n X I.
proof: Proof. pose (C := iConsts I). destruct I as [Gamma s t A H1 H2]; intros (Delta & sigma & T & EQ). exists Delta. exists (inv_subst C sigma). split; [auto using inv_subst_typing|]. rewrite <-!enc_term_app. cbn [s₀ t₀ remove_constants] in EQ. unfold C; now rewrite EQ. 1,3: auto. all: intros; eapply filter_In; cbn; (intuition (auto with datatypes)); destruct eq_dec; intuition (auto with datatypes). 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)