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