simp [varEquals, eval_embSubsts, Matrix.comp_vecCons', Matrix.constant_eq_singleton, Semiterm.val_func, sub_func_iff]
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 : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (Semiterm.func f w)) ↔
    y = Semiterm.valbm (ι.Sub M) x (Semiterm.func f w)
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 : ℕ
f : L'.Func k
w : Fin k → Semiterm L' Empty n
ih :
  ∀ (a : Fin k) {y : ι.Sub M} {x : Fin n → ι.Sub M},
    (Evalbm M (↑y :> fun i => ↑(x i))) (ι.varEquals (w a)) ↔ y = Semiterm.valbm (ι.Sub M) x (w a)
y : ι.Sub M
x : Fin n → ι.Sub M
⊢ (∀ (e : Fin k → M),
      (∀ (i : Fin k), (Evalb s ![e i]) ι.domain ∧ (Evalb s (e i :> fun i => ↑(x i))) (ι.varEquals (w i))) →
        (Evalb s (↑y :> fun i => e i)) (ι.func f)) ↔
    (Evalbm M (↑y :> fun i => ↑(Semiterm.val subStructure x Empty.elim (w i)))) (ι.func f)