case func k f v ih =>
  exact Monotone.monotone f _ _ ih
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
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ n
ih : ∀ (a : Fin k), Semiterm.valm M e₁ ε₁ (v a) ≤ Semiterm.valm M e₂ ε₂ (v a)
⊢ (func f fun i => Semiterm.val inst✝¹ e₁ ε₁ (v i)) ≤ func f fun i => Semiterm.val inst✝¹ e₂ ε₂ (v i)
no goals