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

Re: [PVS-HELP] Choose Function



SongFu schrieb:
> I want know how to proof the following:
>
> choose({x: nat| x=1}) =1

Use the lemma "choose_singleton[nat]" and then expand "singleton".
-- 
Christian Henkel