rfl
case h₀.refl.free.left
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = FreeF.Free (id <$> f)
no goals