case func k f v ih =>
  simp[Rew.func]
  funext i; simp[ih]; rfl
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
⊢ ↑(subtEquiv ((Rew.bind b e) (func f v))) =
    UTerm.func f fun i =>
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(ofSubterm (v i))
no goals