Theorem: LO.FirstOrder.Semiterm.valm_uLift (Logic/FirstOrder/Basic/Model.lean)

State before:
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 }
Tactic:
induction t <;> simp [*, Semiterm.val_func]
State after:
no goals