no goals
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → Structure L (M a)
n : ℕ
f : Functions L n
x : Fin n → (a : α) → M a
⊢ (funMap f fun i => Quotient.mk' (x i)) = Quotient.mk' fun a => funMap f fun i => x i a
apply funMap_quotient_mk'