induction t <;> simp [*, funk_mk, Semiterm.val_func]
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⟧
no goals