∀ {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [inst : (a : α) → L.Structure (M a)]
  [∀ (a : α), Nonempty (M a)] {β : Type u_3} (φ : L.Formula β) (x : β → (a : α) → M a),
  (φ.Realize fun i => Quotient.mk' (x i)) ↔ ∀ᶠ (a : α) in ↑u, φ.Realize fun i => x i a