[\lambda x:nat. nat]
match O:nat with
[ O \Rightarrow O
| (S x) \Rightarrow (S (S x)) ]
###### INTERPRETATION NUMBER 1 ######
### (* disambiguation environment  *)
alias id O = cic:/Coq/Init/Datatypes/nat.ind#1/1/1
alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2
alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
### (* 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