simp[Rew.func, hb]
case func
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ₁ n₁
a_ih✝ : ∀ (a : Fin arity✝), Function.funEqOn (a✝ a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (a✝ a) = ω₂ (a✝ a)
he : Function.funEqOn (func a✝¹ a✝).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ ω₁ (func a✝¹ a✝) = ω₂ (func a✝¹ a✝)
case func
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ₁ n₁
a_ih✝ : ∀ (a : Fin arity✝), Function.funEqOn (a✝ a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (a✝ a) = ω₂ (a✝ a)
he : Function.funEqOn (func a✝¹ a✝).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ (fun i => ω₁ (a✝ i)) = fun i => ω₂ (a✝ i)