proposition: Lemma subst_consts_comp X Y Z (zeta: X -> exp Y) (kappa: Y -> exp Z) s: subst_consts kappa (subst_consts zeta s) = subst_consts (zeta >> subst_consts kappa) s.
proof: Proof. induction s in zeta, kappa |-*; cbn; trivial. - f_equal. rewrite IHs. f_equal. fext. unfold funcomp at 4; unfold funcomp at 4. intros; rewrite <-ren_subst_consts_commute. reflexivity. - now rewrite IHs1, IHs2. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)