∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w'} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → C}
  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : C} {f : X ⟶ Y}
  (toTransfiniteCompositionOfShape : CategoryTheory.TransfiniteCompositionOfShape J f)
  (attachCells :
    (j : J) →
      ¬IsMax j →
        HomotopicalAlgebra.AttachCells (basicCell j) (toTransfiniteCompositionOfShape.F.map (CategoryTheory.homOfLE ⋯)))
  (toTransfiniteCompositionOfShape_1 : CategoryTheory.TransfiniteCompositionOfShape J f)
  (attachCells_1 :
    (j : J) →
      ¬IsMax j →
        HomotopicalAlgebra.AttachCells (basicCell j)
          (toTransfiniteCompositionOfShape_1.F.map (CategoryTheory.homOfLE ⋯))),
  ({ toTransfiniteCompositionOfShape := toTransfiniteCompositionOfShape, attachCells := attachCells } =
      { toTransfiniteCompositionOfShape := toTransfiniteCompositionOfShape_1, attachCells := attachCells_1 }) =
    (toTransfiniteCompositionOfShape = toTransfiniteCompositionOfShape_1 ∧ attachCells ≍ attachCells_1)