simp [Function.comp, eval_nrel, ofEquiv_rel φ, Structure.ofEquiv_val φ]
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
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L μ x✝
⊢ (Eval (ofEquiv φ) e ε) (nrel r v) ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) (nrel r v)
no goals