Theorem: CategoryTheory.List.joinF.associatorRight_nil (Moncalc/CategoryTheory/List/Monad.lean)

State before:
α : Type u
inst✝ : Category α
⊢ joinF.associatorRight [] = 𝟙 []
Tactic:
unfold joinF.associatorRight
State after:
α : Type u
inst✝ : Category α
⊢ associatorRight.aux [] [] [] = 𝟙 []

State before:
α : Type u
inst✝ : Category α
⊢ associatorRight.aux [] [] [] = 𝟙 []
Tactic:
rfl
State after:
no goals