∀ {n : ℕ} (c : OrderedFinpartition (n + 1)) (hc : Set.range (c.emb 0) = {0}) (i j : Fin (c.length - 1)),
  i ≠ j →
    Function.onFun Disjoint
      (fun m =>
        Set.range fun j =>
          have this := ⋯;
          (c.emb (Fin.cast this m.succ) j).pred ⋯)
      i j