∀ (rs : Array Lean.Elab.Command.PreElabHeaderResult) (i : ℕ) (indFVars : Array Lean.Expr),
  i < rs.size →
    ∀ (indFVar : Lean.Expr),
      InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun i indFVars => rs.size - i)
        ⟨i + 1, indFVars.push indFVar⟩ ⟨i, indFVars⟩