simp [bind]
case Vis
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih : ∀ (a : T✝), (bind (k✝ a) fun x => t₂) = bind (Function.const R₁ id <$> k✝ a) fun y => bind t₂ (ret ∘ y)
⊢ (bind (Vis e✝ k✝) fun x => t₂) = bind (Function.const R₁ id <$> Vis e✝ k✝) fun y => bind t₂ (ret ∘ y)
case Vis
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih : ∀ (a : T✝), (bind (k✝ a) fun x => t₂) = bind (Function.const R₁ id <$> k✝ a) fun y => bind t₂ (ret ∘ y)
⊢ (fun r => bind (k✝ r) fun x => t₂) = fun r => bind (k✝ r) fun x => bind t₂ (ret ∘ id)