conv =>
  lhs
  rw [←construct_destruct (corec (bind.automaton k) (.inl (construct <| .Pure x)))]
  rw [destruct_corec]
  rhs
  rhs
  simp only [bind.automaton, destruct_construct]
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
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ construct (corec (bind.automaton k) <$> Sum.inr <$> destruct (k x)) = k x