simpa [eval_rel, Matrix.vecAppend_eq_ite] using this (Matrix.vecAppend rfl v w) (fun i => by simpa [Matrix.vecAppend_eq_ite] using h i)
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
this :
  ∀ (e : Fin (k + k) → M),
    (∀ (i : Fin k), op(=).val ![e (Fin.castLE ⋯ i), e (Fin.natAdd k i)]) →
      (rel r fun i => e (Fin.castLE ⋯ i)) → rel r fun i => e (Fin.natAdd k i)
⊢ rel r v → rel r w
no goals