cases destruct x with
| Pure r =>
  exact pure r
| Free f =>
  exact free f
F : Type u → Type u
inst : QPF F
R : Type u
motive : Free F R → Sort u_1
pure : (r : R) → motive (Pure.pure r)
free : (f : F (Free F R)) → motive (Free.free f)
x : Free F R
⊢ motive (construct (destruct x))
no goals