proposition: Lemma remove_constants_reduction n: 1 <= n -> (forall x, tight RE x = None -> ord (ctype X x) < n) -> OU n X ⪯ OU n Y.
proof: Proof. Proof using consts_agree. intros L ?. assert (forall I: orduni n X, ord' (map (ctype X) (iConsts I)) < n) as O. - intros ?; destruct n; try lia. eapply le_n_S, ord'_elements. intros; mapinj. cbn in H2; simplify in H2. eapply filter_In in H2 as []. destruct (R' x == None); try discriminate. now eapply le_S_n, H. - exists (fun I => remove_constants n I (O I)). intros I; split. eapply remove_constants_forward. eapply remove_constants_backward. 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)