∀ {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [inst : (a : α) → L.Structure (M a)]
  {β : Type u_3} (x : β → (a : α) → M a) (t : L.Term β),
  FirstOrder.Language.Term.realize (fun i => Quotient.mk' (x i)) t =
    Quotient.mk' fun a => FirstOrder.Language.Term.realize (fun i => x i a) t