simp only [pure, bind]
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ pure x >>= k = k x
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ corec (bind.automaton k) (Sum.inl (construct (FreeF.Pure x))) = k x