∀ {ι : Type u_1} {X : ι → Type u_5} {i j k : ι} (hij : i = j) (hjk : j = k) (x : X i),
  (ComplexShape.Embedding.AreComplementary.desc.aux X j k hjk)
      ((ComplexShape.Embedding.AreComplementary.desc.aux X i j hij) x) =
    (ComplexShape.Embedding.AreComplementary.desc.aux X i k ⋯) x