. conv =>
    rhs
    congr
    rw [←QPF.map_id f]
  rw [free, construct, QPF.M.destruct_construct]
  rfl
case h₀.refl.free.left
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = QPF.M.destruct (free f)

case h₀.refl.free.right
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))
case h₀.refl.free.right
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))