simp[models_def, Semiformula.val_Uprod, Empty.eq_elim]
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝² : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
inst✝¹ : Nonempty I
inst✝ : ∀ (i : I), Nonempty (A i)
σ : Sentence L
⊢ Uprod A 𝓤 ⊧ₘ σ ↔ {i | A i ⊧ₘ σ} ∈ 𝓤
no goals