|
SongFu wrote: > Dear everyone: > I want know how to proof the following: > > choose({x: nat| x=1}) =1 > > Thanks > Song If you look at the definition of choose (in the prelude), you'll see its type makes this easy. (typepred "choose({x: nat | x = 1})") then (hide 2) (grind) John |