proposition: Lemma linearize_consts (S: list (exp X)): consts (linearize_terms S) === Consts S.
proof: Proof. unfold linearize_terms. cbn; simplify. split; unfold Consts; intros ? [x] % in_flat_map; eapply in_flat_map. all: intuition; try mapinj. eexists; split; [eassumption|]. now rewrite consts_ren in H1. exists (ren shift x); intuition (auto with listdb). now rewrite consts_ren. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)