exists (λ x => ⟨(x, bind x Free.Monad.pure), by rfl⟩) <$> destruct x
case h₀.refl
F : Type u → Type u
inst : QPF F
R : Type u
x y : QPF.M (FreeF F R)
⊢ QPF.M.liftr (FreeF F R) (fun x y => x >>= pure = y) (QPF.M.destruct x) (QPF.M.destruct (x >>= pure))
case h₀.refl
F : Type u → Type u
inst : QPF F
R : Type u
x y : QPF.M (FreeF F R)
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct x =
      QPF.M.destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct x =
      QPF.M.destruct (x >>= pure)