proposition: Lemma subst_consts_subst Z (s: exp X) sigma tau theta zeta (kappa: X -> exp Z): (forall x, x ∈ vars s -> sigma • subst_consts zeta (tau x) >* subst_consts kappa (theta x)) -> (forall x, x ∈ consts s -> sigma • zeta x >* kappa x) -> sigma • subst_consts zeta (tau • s) >* subst_consts kappa (theta • s).
proof: Proof. Proof using n RE C. induction s in sigma, zeta, tau, kappa, theta |-*. - cbn; intros; eapply H; now econstructor. - cbn; intros; eapply H0; auto. - cbn -[vars]; intros. rewrite IHs with (kappa := kappa >> ren shift) (theta := up theta); [easy|..]. + intros []; cbn; [easy|]. unfold funcomp at 2. rewrite ren_subst_consts_commute. unfold funcomp at 2. rewrite ren_subst_consts_commute. unfold up. asimpl. erewrite <-compSubstSubst_exp; try reflexivity. intros; eapply subst_steps, H. auto. + intros x. unfold funcomp. asimpl. erewrite <-compSubstSubst_exp; try reflexivity. intros; eapply subst_steps, H0; auto. - intros; cbn; rewrite IHs1, IHs2; try reflexivity. 1, 3: intros; eapply H; auto. all: intros; eapply H0; cbn; simplify; intuition. 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)