simp [(v i).prop]
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
k : ℕ
f : L'.Func k
v : Fin k → ι.Sub M
i : Fin k
⊢ ι.Dom ((fun i => ↑(v i)) i)
no goals