∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] (p : (i : ι) → Submodule R (φ i)), Submodule.pi ∅ p = ⊤