have := QPF.map_id (destruct (k x))
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ construct ((fun x => x) <$> destruct (k x)) = k x
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
this : id <$> destruct (k x) = destruct (k x)
⊢ construct ((fun x => x) <$> destruct (k x)) = k x