proposition: Lemma subst_consts_consts X Y (zeta: X -> exp Y) (s: exp X): consts (subst_consts zeta s) === Consts (map zeta (consts s)).
proof: Proof. unfold Consts; induction s in zeta |-*; cbn; simplify; [eauto with listdb|eauto with listdb|..]. - rewrite IHs. unfold funcomp; rewrite <-map_map, !flat_map_concat_map, map_map. erewrite map_ext with (g := consts); intuition eauto with listdb. now rewrite consts_ren. - rewrite IHs1, IHs2, !flat_map_concat_map; simplify. now rewrite concat_app. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)