∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6}
  {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c₃ : ComplexShape I₃} {c₁₂ : ComplexShape I₁₂} {c₂₃ : ComplexShape I₂₃}
  {c : ComplexShape J} [inst : TotalComplexShape c₁ c₂ c₁₂] [inst_1 : TotalComplexShape c₁₂ c₃ c]
  [inst_2 : TotalComplexShape c₂ c₃ c₂₃] [inst_3 : TotalComplexShape c₁ c₂₃ c],
  (∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃), c₁₂.π c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.π c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃))) →
    (∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
        c₁.ε₁ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)) →
      (∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
          c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₁ c₃ c₂₃ (i₂, i₃) =
            c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)) →
        (∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
            c₁₂.ε₂ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₂ c₃ c₂₃ (i₂, i₃)) →
          c₁.Associative c₂ c₃ c₁₂ c₂₃ c