∀ (n : ℕ),
  Function.RightInverse
    (fun i =>
      ⟨{ blocks := (List.ofFn fun j => (i.snd j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ },
        { blocks := List.ofFn fun j => (i.snd j).length, blocks_pos := ⋯, blocks_sum := ⋯ }⟩)
    fun i => ⟨i.fst.gather i.snd, i.fst.sigmaCompositionAux i.snd⟩