induction as
α : Type u
inst✝ : Category α
as : List α
⊢ joinF.unitorRightLax as ≫ joinF.unitorRightOplax as = 𝟙 as
case nil
α : Type u
inst✝ : Category α
⊢ joinF.unitorRightLax [] ≫ joinF.unitorRightOplax [] = 𝟙 []

case cons
α : Type u
inst✝ : Category α
head✝ : α
tail✝ : List α
tail_ih✝ : joinF.unitorRightLax tail✝ ≫ joinF.unitorRightOplax tail✝ = 𝟙 tail✝
⊢ joinF.unitorRightLax (head✝ :: tail✝) ≫ joinF.unitorRightOplax (head✝ :: tail✝) = 𝟙 (head✝ :: tail✝)