cases x using by_cases with
| pure r =>
  have : destruct (pure r) = .Pure r := by
    exact @destruct_construct F _ R (FreeF.Pure r)
  simp only [Functor.map, this, pure_bind r]
  constructor <;> rfl
| free f =>
  have : destruct (free f) = .Free f := by
    exact @destruct_construct F _ R (FreeF.Free f)
  simp only [Functor.map, this, free_bind, ←QPF.map_comp, Function.comp]
  constructor
  . conv =>
      rhs
      congr
      rw [←QPF.map_id f]
    rw [free, construct, QPF.M.destruct_construct]
    rfl
  . simp only [free, construct, QPF.M.destruct_construct]
    rfl
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)
no goals