∀ {ι : Type u_2} {M : Type u_1} {a : M} {m : ι → Multiset M} (a_1 : ι) (s : Finset ι) (h : a_1 ∉ s),
  (a ∈ ∑ i ∈ s, m i ↔ ∃ i ∈ s, a ∈ m i) → (a ∈ ∑ i ∈ Finset.cons a_1 s h, m i ↔ ∃ i ∈ Finset.cons a_1 s h, a ∈ m i)