∀ {ι : Type u_1} {n : ℕ} [inst : NeZero n] [inst_1 : Fintype ι] {B I : BoxIntegral.Box ι},
  I ∈ BoxIntegral.unitPartition.prepartition n B ↔
    ∃ ν ∈ BoxIntegral.unitPartition.admissibleIndex n B, BoxIntegral.unitPartition.box n ν = I