exact congr_arg Subtype.val (eval_varEquals_iff.mp this)
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
n k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h : (Evalbm M fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) (ι.rel r)
l : Fin k → M
H : ∀ (i : Fin k), (Evalb s ![l i]) ι.domain ∧ (Evalb s (l i :> fun i => ↑(e i))) (ι.varEquals (v i))
i : Fin k
z : ι.Sub M := ⟨l i, ⋯⟩
this : (Evalbm M (↑z :> fun i => ↑(e i))) (ι.varEquals (v i))
⊢ l i = ↑(Semiterm.valbm (ι.Sub M) e (v i))
no goals