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

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