[\lambda x:bool. nat]
match true:bool with
[ true \Rightarrow O
| false \Rightarrow (S O) ]
### (* METASENV after disambiguation  *)

### (* TERM after disambiguation      *)

<[x:bool]nat>Cases true of 
 true => O
 false => (S O)
end
### (* TYPE_OF the disambiguated term *)
([x:bool]nat true)
### (* REDUCED disambiguated term     *)
O