The one-letter normalisation

At arity one the collapse and the insertion are mutually inverse: the single head is already at the front, and re-inserting it puts it back where it was.

theorem RS.freeCollapse_freeInsert_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) : CategoryTheory.CategoryStruct.comp (freeCollapse A V 1) (freeInsert A V 0) = CategoryTheory.CategoryStruct.id (tensorPow D (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) 1)

The one-letter normalisation is trivial.