induction as
α : Type u
inst✝ : Category α
as : List α
⊢ joinF.unitorLeftOplax as ≫ joinF.unitorLeftLax as = 𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor as)
case nil
α : Type u
inst✝ : Category α
⊢ joinF.unitorLeftOplax [] ≫ joinF.unitorLeftLax [] = 𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor [])

case cons
α : Type u
inst✝ : Category α
head✝ : α
tail✝ : List α
tail_ih✝ :
  joinF.unitorLeftOplax tail✝ ≫ joinF.unitorLeftLax tail✝ = 𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor tail✝)
⊢ joinF.unitorLeftOplax (head✝ :: tail✝) ≫ joinF.unitorLeftLax (head✝ :: tail✝) =
    𝟙 (Prefunctor.obj (singletonF ⋙ joinF).toPrefunctor (head✝ :: tail✝))