3 match x:nat with [ O \Rightarrow nat | (S x) \Rightarrow bool ]]
6 | (S x) \Rightarrow false ]
7 ### (* METASENV after disambiguation *)
9 ### (* TERM after disambiguation *)
12 <[y:nat]Set>Cases x of
19 ### (* TYPE_OF the disambiguated term *)
21 <[y:nat]Set>Cases x of
25 ### (* REDUCED disambiguated term *)