[PVS-Help] Termination TCC

[Jerome <jerome@xxxxxxxxxxxxxx>]

All,
I have the following recursive definition:

example: THEORY BEGIN
  index:   TYPE  = posnat
  value:   TYPE  = real
  indices: TYPE+ = finite_set[index]
  myset:   TYPE  = [index -> value]
  fun:     TYPE  = FUNCTION[value, value -> value]

  curry(f: fun, m: myset, I: indices): RECURSIVE value =
    LET i: index = choose(I) IN
      IF singleton?(I) THEN m(i)
      ELSE f(m(i), curry(f, m, remove(i, I)))
      ENDIF
  MEASURE card(I)
END example

When I go to typecheck it, one of the TCC's it gives me is the
following:

curry_TCC2: OBLIGATION
  FORALL (I: indices, i: index):
    NOT singleton?(I) AND i = choose(I) IMPLIES
     card[index](remove[index](i, I)) < card[index](I);

Why isn't this proved with the "card_remove" theorem from the prelude?
I've tried to prove the obligation by hand, and bring in card_remove
manually, but PVS doesn't seem to know about it:

Rule? (lemma "card_remove")
Found 0 resolutions for card_remove relative to the substitution.

Any insight would be appreciated.

jerome

[Also, if anyone knows of a better way to apply a binary function over
 a set of values please speak up. For example, given the set {a, b, c,
 d}, I'd like to return min(a, min(b, min(c, d))).]