# [PVS-Help] How can we extract properties from singleton_elt[nat]?

```Hi All,

I got so confused when proving something in PVS like:

{-1}  j = get_index(3)
|-------
{1}   j = 1

```
and when I expanded "get_index", it showed me "singleton_elt[nat](.....)" as follows:
```
{-1}  j =
singleton_elt[nat]
({i: nat |
EXISTS (j: nat):
j < 3 AND
i < 3 AND
i < j AND
(FORALL (k: nat): k /= j AND k < 3 IMPLIES k <= i)})
|-------
[1]   j = 1
(Basically, "get_index(n)" returns n-2)

```
To prove this, is there any way to somehow "extract" the properties shown in fnum[-1] as some antecedent? Thus, we can do "skolem" and "case" analysis to prove it.
```

```
By the way, I tried so many PVS prover command to deal with this singleton but failed. When I tried to expand "singleton_elt", it showed:
```
{-1}  j =
the! (x: nat):
EXISTS (j: nat):
j < 3 AND
x < 3 AND
x < j AND (FORALL (k: nat): k /= j AND k < 3 IMPLIES k <= x)
|-------
[1]   j = 1

What can we do using PVS prove command with "the!(x:nat)" ?

Really appreciate!

Thank you!

Xiwen

*********************************************************************
The whole theory is shown below if needed:

(Intuitively, "get_index(n)" returns n-2)

TEST: THEORY
BEGIN
get_index(length:nat): nat = {i:nat| EXISTS (j:nat): j<length AND
i<length AND i<j AND
(FORALL (k:nat): k/=j AND k<length
IMPLIES  k<=i
)
}

get_index_3: LEMMA FORALL (j:nat): j=get_index(3) IMPLIES j=1

END TEST
*********************************************************************

```