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 : β
⊢ (↑(foldlM.ofFreeMonoid f) ∘ FreeMonoid.of) x = (foldlM.mk ∘ flip 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 α
⊢ ↑(foldlM.ofFreeMonoid f) ∘ FreeMonoid.of = foldlM.mk ∘ flip f
ext1 x