induction t₁ with
| Ret _ => rfl
| 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 a => bind t₂ fun x => ret a) = bind (Function.const R₂ <$> t₁) fun y => bind t₂ (ret ∘ y)
no goals