Theorem: LO.FirstOrder.Structure.Eq.QuotEq.val_mk (Logic/FirstOrder/Basic/Eq.lean)

State before:
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
t : Semiterm L μ n
⊢ valm (QuotEq H) (fun i => ⟦e i⟧) (fun i => ⟦ε i⟧) t = ⟦valm M e ε t⟧
Tactic:
induction t <;> simp [*, funk_mk, Semiterm.val_func]
State after:
no goals