simp [eval_ofEquiv_iff (p := p), eval_ofEquiv_iff (p := q)]
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p q : Semiformula L μ x✝
⊢ (Eval (ofEquiv φ) e ε) (p ⋎ q) ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) (p ⋎ q)
no goals