have : M ⊧ₘ ∀* (Semiformula.vecEq varSumInL varSumInR ⟶ Semiformula.rel r varSumInL ⟶ Semiformula.rel r varSumInR) :=
  H.realize (eqAxiom.relExt r (L := L))
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)
⊢ rel r v → rel r w
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 : M ⊧ₘ ∀* (vecEq varSumInL varSumInR ⟶ Semiformula.rel r varSumInL ⟶ Semiformula.rel r varSumInR)
⊢ rel r v → rel r w