# Re: [PVS-Help] how to prove such a simple lemma?

```K.Wei wrote:
> Hello all,
>
> I just met a so simple lemma, but don't know how to prove it. Who could help me?
>
> P,Q: VAR [size:{a:nat| a>=3}, [below[size] ->set[nat]]]
>
> test: LEMMA   P`1=Q`1+1 AND FORALL (i:below(P`1)),(j:below(Q`1)): P`2(i)=Q`2(j)
>                           IMPLIES EXISTS (i,j:below(P`1)): P`2(i)=P`2(j)
>
> since the size of Q is 1 less than the size of P, so this lemma should hold. I think I should use epsilons, but don't know how to apply this command.
>
> many thanks!
>
>
> Kun
>
>

Kun,

The epsilon function is not required in this case.
You can instantiate i and j in the EXISTS ...
with two constants. For example, i=0, j=0 should work
fine.

For this to work, you need to fix the formula above
(otherwise PVS will parse it into something not provable).

Assuming it's rewritten as

test: LEMMA
P`1=Q`1+1 AND (FORALL (i:below(P`1)),(j:below(Q`1)):P`2(i)=Q`2(j))
IMPLIES EXISTS (i,j:below(P`1)): P`2(i)=Q`2(j)

Then (skosimp)(inst + "0" "0")(reduce) should work,

Bruno

```