induction t <;> simp [*, Semiterm.val_func]
L : Language
M : Type u_1
inst✝² : LE M
inst✝¹ : Structure L M
inst✝ : Monotone L M
ξ : Type u_2
n : ℕ
t : Semiterm L ξ n
e₁ e₂ : Fin n → M
ε₁ ε₂ : ξ → M
he : ∀ (i : Fin n), e₁ i ≤ e₂ i
hε : ∀ (i : ξ), ε₁ i ≤ ε₂ i
⊢ Semiterm.valm M e₁ ε₁ t ≤ Semiterm.valm M e₂ ε₂ t
case func
L : Language
M : Type u_1
inst✝² : LE M
inst✝¹ : Structure L M
inst✝ : Monotone L M
ξ : Type u_2
n : ℕ
e₁ e₂ : Fin n → M
ε₁ ε₂ : ξ → M
he : ∀ (i : Fin n), e₁ i ≤ e₂ i
hε : ∀ (i : ξ), ε₁ i ≤ ε₂ i
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ n
a_ih✝ : ∀ (a : Fin arity✝), Semiterm.valm M e₁ ε₁ (a✝ a) ≤ Semiterm.valm M e₂ ε₂ (a✝ a)
⊢ (func a✝¹ fun i => Semiterm.val inst✝¹ e₁ ε₁ (a✝ i)) ≤ func a✝¹ fun i => Semiterm.val inst✝¹ e₂ ε₂ (a✝ i)