Looking for old finite_set library

[Guru P P <ppguru@csa.iisc.ernet.in>]

Hello,
I am working on PVS proof reuse.
I need the old pvs finite_set library.

Specially I am interested in the following two LEMMA's
A,B: VAR finite_set

finite_union: LEMMA is_finite(union(A,B))
finite_intersection: LEMMA is_finite(intersection(A,B))

Can somebody suggest me a url, where I can find this proof.

Thanks
Guru

|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
                    A mind all logic is like a knife all blade. 
                       It makes the hand bleed that uses it.

|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||