# [PVS-Help] Showing all type predicates for a skolem constant

```Hello,

I'd like to know how to make all type predicates explicit.
Consider the following theory:
-------------------------------------------
typepreds: THEORY
BEGIN
nat: LEMMA
FORALL (n: nat):
n >= 0

below: LEMMA
FORALL (n: below (3)):
n >= 0
END typepreds
-------------------------------------------

and the following proof for "nat":

-------------------------------------------
nat :
|-------
{1}   FORALL (n: nat): n >= 0

Rule? (skolem + "N")
For the top quantifier in +, we introduce Skolem constants: N,
this simplifies to:
nat :
|-------
{1}   N >= 0

Rule? (typepred "N")
this simplifies to:
nat :
{-1}  N >= 0
|-------
[1]   N >= 0

which is trivially true.
Q.E.D.
-------------------------------------------

If I use the same proof steps for "below" I get:

-------------------------------------------
below :
|-------
{1}   FORALL (n: below(3)): n >= 0

Rule? (skolem + "N")
For the top quantifier in +, we introduce Skolem constants: N,
this simplifies to:
below :
|-------
{1}   N >= 0

Rule? (typepred "N")
this simplifies to:
below :
{-1}  N < 3
|-------
[1]   N >= 0
-------------------------------------------

Now below(3) = {s: nat | s < 3} so the type predicate "N >= 0"
also holds, but PVS doesn't show it. Evidently PVS does know
the predicate, because an assert proves the lemma.

-------------------------------------------
below :
{-1}  N < 3
|-------
[1]   N >= 0
Rule? (assert)
Simplifying, rewriting, and recording with decision procedures,
Q.E.D.
-------------------------------------------

My question is how to make all type predicates explicit,
so that the sequent is:

-------------------------------------------
{-1}  N < 3
{-2}  N >= 0
|-------
[1]   N >= 0
-------------------------------------------