induction p using Semiformula.rec'
  <;> simp [*, Matrix.constant_eq_singleton, eval_substs, eval_translationRel_iff, eval_rel, eval_nrel]
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 : ℕ
p : Semisentence L' n
e : Fin n → ι.Sub M
⊢ (Evalbm M fun i => ↑(e i)) (ι.translation p) ↔ (Evalbm (ι.Sub M) e) p
case hall
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 n✝ : ℕ
p✝ : Semiformula L' Empty (n✝ + 1)
a✝ : ∀ {e : Fin (n✝ + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p✝) ↔ (Evalbm (ι.Sub M) e) p✝
e : Fin n✝ → ι.Sub M
⊢ (∀ (x : M), (Eval s ![x] Empty.elim) ι.domain → (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p✝)) ↔
    ∀ (a : M) (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p✝

case hex
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 n✝ : ℕ
p✝ : Semiformula L' Empty (n✝ + 1)
a✝ : ∀ {e : Fin (n✝ + 1) → ι.Sub M}, (Evalbm M fun i => ↑(e i)) (ι.translation p✝) ↔ (Evalbm (ι.Sub M) e) p✝
e : Fin n✝ → ι.Sub M
⊢ (∃ x, (Eval s ![x] Empty.elim) ι.domain ∧ (Eval s (x :> fun i => ↑(e i)) Empty.elim) (ι.translation p✝)) ↔
    ∃ a, ∃ (b : ι.Dom a), (Eval subStructure (⟨a, b⟩ :> e) Empty.elim) p✝