proposition: Lemma subst_const_comm_id Y zeta sigma (s: exp Y): subst_consts zeta s = s -> (sigma >> subst_consts zeta) • s = subst_consts zeta (sigma • s).
proof: Proof. induction s in zeta, sigma |-*; cbn; [trivial|congruence|..]. - injection 1 as H. f_equal. rewrite <-IHs; trivial. now rewrite subst_consts_up. - injection 1 as H. f_equal; eauto. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)