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

### (* TERM after disambiguation      *)

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