rfl
Ω : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝ : MeasurableSpace Ω
π : ι → Set (Set Ω)
μ : Measure Ω
S : Finset ι
s : ι → Set Ω
f : (i : ι) → Ω → β i
⊢ iIndep (fun i => generateFrom {s i}) μ ↔ iIndepSet s μ
no goals