∀ (x : ℕ),
  Plausible.InjectiveFunction.sliceSizes x =
    let n := x;
    if h : 0 < n then
      have this := ⋯;
      MLList.cons ⟨n, h⟩ (Plausible.InjectiveFunction.sliceSizes (n / 2))
    else MLList.nil