Theorem: Free.destruct_free (CoInd/QPF/FreeMonads.lean)

State before:
F : Type u → Type u
inst : QPF F
R : Type u
f : F (Free F R)
⊢ destruct (free f) = FreeF.Free f
Tactic:
simp [free, destruct_construct]
State after:
no goals