4 | (S x) \Rightarrow (S (S x)) ]
5 ###### INTERPRETATION NUMBER 1 ######
6 ### (* disambiguation environment *)
7 alias id O = cic:/Coq/Init/Datatypes/nat.ind#1/1/1
8 alias id S = cic:/Coq/Init/Datatypes/nat.ind#1/1/2
9 alias id nat = cic:/Coq/Init/Datatypes/nat.ind#1/1
10 ### (* METASENV after disambiguation *)
12 ### (* TERM after disambiguation *)
14 <[x:nat]nat>Cases O of
18 ### (* TYPE_OF the disambiguated term *)
20 ### (* REDUCED disambiguated term *)