induction t₁ with
| Ret _ =>
  simp [Function.const, Function.comp, bind]
| Vis _ _ ih =>
  simp [bind]; funext _; simp [ih]; sorry
E : Type → Type
R₁ R₂ : Type
t₁ : Fitree E R₁
t₂ : Fitree E R₂
⊢ (bind t₁ fun x => t₂) = bind (Function.const R₁ id <$> t₁) fun y => bind t₂ (ret ∘ y)
no goals