simp[Rew.func'']
case hb.mk
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₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
val✝ : ℕ
isLt✝ : val✝ < n₁
⊢ ω #⟨val✝, isLt✝⟩ = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) #⟨val✝, isLt✝⟩

case hf
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₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : ξ₁
⊢ ω &t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) &t
case hf
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₂
b : Fin n₁ → Semiterm L ξ₂ n₂
e : ξ₁ → Semiterm L ξ₂ n₂
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : ξ₁
⊢ ω &t = (bind (⇑ω ∘ bvar) (⇑ω ∘ fvar)) &t