sorry
case Vis.h
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 a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> k✝ a) fun y => bind t₂ (ret ∘ y)
x✝ : T✝
⊢ (bind (Function.const R₂ <$> k✝ x✝) fun y => bind t₂ (ret ∘ y)) =
    bind (k✝ x✝) fun x => bind t₂ (ret ∘ Function.const R₂ x)
no goals