have : destruct (pure r) = .Pure r := by
  exact @destruct_construct F _ R (FreeF.Pure r)
case h₀.refl.pure
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
r : R
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (pure r) =
      QPF.M.destruct (pure r) ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (pure r) =
      QPF.M.destruct (pure r >>= pure)
case h₀.refl.pure
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
r : R
this : destruct (pure r) = FreeF.Pure r
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (pure r) =
      QPF.M.destruct (pure r) ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (pure r) =
      QPF.M.destruct (pure r >>= pure)