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

### (* TERM after disambiguation      *)

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