∀ {ι : Type u_2} {M : Type u_1} [inst : CommMonoid M] {f : ι → M} (a : ι) (s : Finset ι) (h : a ∉ s),
  (IsUnit (∏ a ∈ s, f a) ↔ ∀ a ∈ s, IsUnit (f a)) →
    (IsUnit (∏ a ∈ Finset.cons a s h, f a) ↔ ∀ a_2 ∈ Finset.cons a s h, IsUnit (f a_2))