induction p using Semiformula.rec' <;> simp [*, Semiformula.eval_rel, Semiformula.eval_nrel, val_mk, rel_mk]
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n : ℕ
e : Fin n → M
ε : μ → M
p : Semiformula L μ n
⊢ (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p ↔ (Evalm M e ε) p
case hall
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n : ℕ
ε : μ → M
n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : ∀ {e : Fin (n✝ + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p✝ ↔ (Evalm M e ε) p✝
e : Fin n✝ → M
⊢ (∀ (x : QuotEq H), (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p✝) ↔ ∀ (x : M), (Eval inst✝ (x :> e) ε) p✝

case hex
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
n : ℕ
ε : μ → M
n✝ : ℕ
p✝ : Semiformula L μ (n✝ + 1)
a✝ : ∀ {e : Fin (n✝ + 1) → M}, (Evalm (QuotEq H) (fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p✝ ↔ (Evalm M e ε) p✝
e : Fin n✝ → M
⊢ (∃ x, (Eval struc (x :> fun i => ⟦e i⟧) fun i => ⟦ε i⟧) p✝) ↔ ∃ x, (Eval inst✝ (x :> e) ε) p✝