∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (self : CategoryTheory.TwistShiftData C A) (a b c : A),
  self.z (a + b) c * self.z a b = self.z a (b + c) * self.z b c