proposition: Lemma remove_constants_forward n (I: orduni n X) (H: ord' (map (ctype X) (iConsts I)) < n): OU n X I -> OU n Y (remove_constants n I H).
proof: Proof. assert (1 <= n) as L by lia. destruct I as [Gamma s t A H1 H2]; intros (Delta & tau' & T' & E'); cbn in *. eapply downcast_constants_ordered in T' as (Sigma & tau & T & E & _ & Cs); [|eauto..]; clear tau' E'. pose (C := filter (fun x => if R' x == None then true else false) (Consts [s; t])). exists (enc_ctx C (Delta ++ Sigma)). exists (enc_subst C tau). split. - eapply remove_constants_ordertypingSubst; trivial. intros ? ? ? % Cs. intros ?; cbn; eapply filter_In. intuition. destruct eq_dec; intuition. - cbn [s₀ t₀ remove_constants iConsts Consts flat_map]; simplify; unfold C. cbn in Cs; simplify in Cs. rewrite !enc_subst_term_reduce; trivial; intuition trivial. now rewrite E. all: eapply filter_In; destruct eq_dec; cbn; intuition (auto with datatypes). all: rewrite app_nil_r; eauto. 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)