simp only [Functor.map, this, free_bind, ←QPF.map_comp, Function.comp]
case h₀.refl.free
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
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (free f) =
      QPF.M.destruct (free f) ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (free f) =
      QPF.M.destruct (free f >>= pure)
case h₀.refl.free
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) ∧
    FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))