Very simple question regarding typepred or the like

[Peter Gumm]

Suppose I have a type defined as 

S : Type = {0,1} 

and I want to prove 

forall (x:S): x=0 or x=1

I would have expected, that after a (skeep) i could use 

(typepred x)

Unfortunately, that does not work. The only way I know how to finish the proof is with 

(assert)

However, this being a black box I'd rather see a basic proof command to make progress.

Which is the one I am missing?

H. Peter