3 match x:nat with [ O \Rightarrow nat | (S x) \Rightarrow bool ]]
6 | (S x) \Rightarrow false ]
7 ###### INTERPRETATION NUMBER 1 ######
8 ### (* disambiguation environment *)
9 alias id O = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)
10 alias id S = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)
11 alias id bool = cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)
12 alias id false = cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/2)
13 alias id nat = cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)
14 ### (* METASENV after disambiguation *)
16 ### (* TERM after disambiguation *)
19 <[y:nat]Set>Cases x of
26 ### (* TYPE_OF the disambiguated term *)
28 <[y:nat]Set>Cases x of
32 ### (* REDUCED disambiguated term *)