∀ {ι : Type u_2} {R : Type u_3} [inst : CommSemiring R] {s : ι → Type u_4} {F : Type u_1} [inst_1 : AddCommMonoid F]
  (φ : R × ((i : ι) → s i) → F),
  (∀ (f : (i : ι) → s i), φ (0, f) = 0) →
    ∀ (f : (i : ι) → s i), (FreeAddMonoid.lift φ) (FreeAddMonoid.of (0, f)) = (FreeAddMonoid.lift φ) 0