[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-HELP] Choose Function



Dear everyone:
I want know how to proof the following:
 
choose({x: nat| x=1}) =1
 
Thanks
Song