induction t <;> simp [*, Semiterm.val_func]
L : Language
M : Type v
inst✝ : Structure L M
n : ℕ
ξ : Type u_1
e : Fin n → ULift.{v', v} M
ε : ξ → ULift.{v', v} M
t : Semiterm L ξ n
⊢ valm (ULift.{v', v} M) e ε t = { down := valm M (fun i => (e i).down) (fun i => (ε i).down) t }
no goals