proposition: Fact msum_morph n f : phi (msum m1 u1 n f) = msum m2 u2 n (fun x => phi (f x)).
proof: Proof. Proof using Hphi1 Hphi2. revert f; induction n as [ | n IHn ]; intros f; simpl; auto. rewrite Hphi2, IHn; trivial. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)