∀ {α : Type u_1} (xs ys acc : Array α) (i j : ℕ),
  ¬i ≥ xs.size →
    ∀ (hj : ¬j ≥ ys.size),
      InvImage (fun x1 x2 => x1 < x2)
        (fun x => PSigma.casesOn x fun acc i => PSigma.casesOn i fun i j => xs.size + ys.size - (i + j))
        ⟨acc.push ys[j], ⟨i, j + 1⟩⟩ ⟨acc, ⟨i, j⟩⟩