Theorem: LO.FirstOrder.Structure.operator_val_ofEquiv_iff (Logic/FirstOrder/Basic/Operator.lean)

State before:
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)
Tactic:
simp [Semiformula.Operator.val, eval_ofEquiv_iff, Empty.eq_elim]
State after:
no goals