simp [Function.comp, eval_nrel, ←EmbeddingClass.rel φ, HomClass.val_term]
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝¹ : ℕ
e₁ : Fin x✝¹ → M₁
ε₁ : μ → M₁
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L μ x✝¹
x✝ : (nrel r v).Open
⊢ (Eval s₁ e₁ ε₁) (nrel r v) ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) (nrel r v)
no goals