exact ih.mp (by simpa [Matrix.comp_vecCons'] using h x hx)
case mp
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✝ n : ℕ
p : Semiformula L' Empty (n + 1)
ih : ∀ {e : Fin (n + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
e : Fin n → ι.Sub M
h : ∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p)
x : M
hx : ι.Dom x
⊢ (Eval subStructure (⟨x, hx⟩ :> e) Empty.elim) p
no goals