case h
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : IsLawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m α
x✝ : β
⊢ (↑(foldrM.ofFreeMonoid f) ∘ FreeMonoid.of) x✝ = (foldrM.mk ∘ f) x✝
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : IsLawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m α
⊢ ↑(foldrM.ofFreeMonoid f) ∘ FreeMonoid.of = foldrM.mk ∘ f
ext