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#1/1/1
10 alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2
11 alias id bool = cic:/Coq/Init/Datatypes/bool.ind#1/1
12 alias id false = cic:/Coq/Init/Datatypes/bool.ind#1/1/2
13 alias id nat = cic:/Coq/Init/Datatypes/nat.ind#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 *)