rw [←construct_destruct <| bind (pure r) k]
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ bind (pure r) k = construct (destruct (k r))
C : _root_.Container
R S : Type u₁
r : R
k : R → Free C S
⊢ construct (destruct (bind (pure r) k)) = construct (destruct (k r))