simp [Semiformula.Operator.val, eval_ofEquiv_iff, Empty.eq_elim]
L : Language
M : Type u_1
inst✝ : Structure L M
N : Type u_2
φ : M ≃ N
k : ℕ
o : Semiformula.Operator L k
v : Fin k → N
⊢ o.val v ↔ o.val (⇑φ.symm ∘ v)
no goals