proposition: Lemma subst_consts_inject_forward sigma s: subst_consts inj (sigma • s) = (sigma >> subst_consts inj) • (subst_consts inj s).
proof: Proof. induction s in sigma |-*; cbn in *; intuition. - f_equal. rewrite inj_ren. rewrite IHs. f_equal. fext; intros []; cbn; auto. rewrite <-inj_ren with (delta := shift) at 1. unfold funcomp at 2. now rewrite ren_subst_consts_commute. - now rewrite IHs1, IHs2. 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)