proposition: Lemma subst_consts_inject_backwards sigma s f: subst_consts (re f) (sigma • subst_consts inj s) = (sigma >> subst_consts (re f)) • s.
proof: Proof. induction s in sigma, f |-*; cbn. - reflexivity. - unfold funcomp. unfold re. unfold tight. rewrite retr. destruct (I c == I c); intuition. - f_equal. rewrite subst_consts_up, inj_ren, re_ren; auto. - rewrite IHs1, IHs2; auto. 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)