simpa [Matrix.comp_vecCons] using h
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n✝ : ℕ
ε : μ → M
n : ℕ
p : Semiformula L μ (n + 1)
ih : ∀ {e : Fin (n + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
e : Fin n → M
a : M
h : (Eval struc (⟦a⟧ :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p
⊢ (Evalm (QuotEq H) (fun i => ⟦(a :> e) i⟧) fun i => ⟦ε i⟧) p
no goals