simp [eval_varEquals_iff, Matrix.constant_eq_singleton]
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 k : ℕ
e : Fin n → ι.Sub M
r : L'.Rel k
v : Fin k → Semiterm L' Empty n
h :
  ∀ (e_1 : Fin k → M),
    (∀ (i : Fin k), (Evalb s ![e_1 i]) ι.domain ∧ (Evalb s (e_1 i :> fun i => ↑(e i))) (ι.varEquals (v i))) →
      (Eval s e_1 Empty.elim) (ι.rel r)
i : Fin k
⊢ (Evalb s ![(fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) i]) ι.domain ∧
    (Evalb s ((fun i => ↑(Semiterm.valbm (ι.Sub M) e (v i))) i :> fun i => ↑(e i))) (ι.varEquals (v i))
no goals