simp [bind, ih]
case Vis
R₁ R₂ R₃ : Type
E : Type → Type
f : R₁ → R₂
g : R₂ → R₃
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih : ∀ (a : T✝), bind (k✝ a) (ret ∘ g ∘ f) = bind (k✝ a) fun x => ret (g (f x))
⊢ bind (Vis e✝ k✝) (ret ∘ g ∘ f) = bind (Vis e✝ k✝) fun x => ret (g (f x))
no goals