∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s₁ s₂ : CompositionSeries X},
  RelSeries.head s₁ = RelSeries.head s₂ → RelSeries.last s₁ = RelSeries.last s₂ → s₁.length = 0 → s₂.length = 0