simp [Function.const, Function.comp, bind]
case Ret
E : Type → Type
R₁ R₂ : Type
t₂ : Fitree E R₂
r✝ : R₁
⊢ (bind (Ret r✝) fun x => t₂) = bind (Function.const R₁ id <$> Ret r✝) fun y => bind t₂ (ret ∘ y)
no goals