unfold joinF.associatorLeft
α : Type u
inst✝ : Category α
ass : List (List α)
asss : List (List (List α))
⊢ joinF.associatorLeft (([] :: ass) :: asss) = joinF.associatorLeft (ass :: asss)
α : Type u
inst✝ : Category α
ass : List (List α)
asss : List (List (List α))
⊢ associatorLeft.aux [] [] (([] :: ass) :: asss) = associatorLeft.aux [] [] (ass :: asss)