proposition: Lemma ren_subst_consts_commute X Y (zeta: X -> exp Y) delta s: subst_consts (zeta >> ren delta) (ren delta s) = ren delta (subst_consts zeta s).
proof: Proof. induction s in delta, zeta |-*; cbn; trivial. - f_equal. rewrite <-IHs. f_equal. asimpl. reflexivity. - now rewrite IHs1, IHs2. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)