Theorem: Free.bind_pure (CoInd/QPF/FreeMonads.lean)

State before:
F : Type u → Type u
inst : QPF F
R : Type u
x : Free F R
⊢ x >>= pure = x
Tactic:
conv =>
  rhs
  rw [bind_pure.internal x (bind x pure)]
  rfl
  rfl
State after:
no goals