match nil:list with
[ nil \Rightarrow nil
| (cons x y) \Rightarrow (cons x y) ]
+###### INTERPRETATION NUMBER 1 ######
+### (* disambiguation environment *)
+alias id cons = cic:/CoRN/algebra/ListType/list.ind#1/1/2
+alias id list = cic:/CoRN/algebra/ListType/list.ind#1/1
+alias id nil = cic:/CoRN/algebra/ListType/list.ind#1/1/1
+### (* METASENV after disambiguation *)
+_ :? _; _ :? _ |- ?25: Type
+### (* TERM after disambiguation *)
+
+<[x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]}>Cases nil{A:=?25[_ ; _]} of
+ nil => nil{A:=?25[_ ; _]}
+ cons => [x:?25[_ ; _]][y:list{A:=?25[x ; _]}](cons{A:=?25[x ; y]} x y)
+end
+### (* TYPE_OF the disambiguated term *)
+([x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]} nil{A:=?25[_ ; _]})
+### (* REDUCED disambiguated term *)
+nil{A:=?25[_ ; _]}
+###### INTERPRETATION NUMBER 2 ######
+### (* disambiguation environment *)
+alias id cons = cic:/Coq/Lists/List/list.ind#1/1/2
+alias id list = cic:/Coq/Lists/List/list.ind#1/1
+alias id nil = cic:/Coq/Lists/List/list.ind#1/1/1
+### (* METASENV after disambiguation *)
+_ :? _; _ :? _ |- ?25: Set
+### (* TERM after disambiguation *)
+
+<[x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]}>Cases nil{A:=?25[_ ; _]} of
+ nil => nil{A:=?25[_ ; _]}
+ cons => [x:?25[_ ; _]][y:list{A:=?25[x ; _]}](cons{A:=?25[x ; y]} x y)
+end
+### (* TYPE_OF the disambiguated term *)
+([x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]} nil{A:=?25[_ ; _]})
+### (* REDUCED disambiguated term *)
+nil{A:=?25[_ ; _]}
+###### INTERPRETATION NUMBER 3 ######
+### (* disambiguation environment *)
+alias id cons = cic:/Coq/Lists/MonoList/list.ind#1/1/2
+alias id list = cic:/Coq/Lists/MonoList/list.ind#1/1
+alias id nil = cic:/Coq/Lists/MonoList/list.ind#1/1/1
### (* METASENV after disambiguation *)
### (* TERM after disambiguation *)
([x:list]list nil)
### (* REDUCED disambiguated term *)
nil
+###### INTERPRETATION NUMBER 4 ######
+### (* disambiguation environment *)
+alias id cons = cic:/Lannion/continuations/weight/specif/list.ind#1/1/2
+alias id list = cic:/Lannion/continuations/weight/specif/list.ind#1/1
+alias id nil = cic:/Lannion/continuations/weight/specif/list.ind#1/1/1
+### (* METASENV after disambiguation *)
+_ :? _; _ :? _ |- ?25: Set
+### (* TERM after disambiguation *)
+
+<[x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]}>Cases nil{A:=?25[_ ; _]} of
+ nil => nil{A:=?25[_ ; _]}
+ cons => [x:?25[_ ; _]][y:list{A:=?25[x ; _]}](cons{A:=?25[x ; y]} x y)
+end
+### (* TYPE_OF the disambiguated term *)
+([x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]} nil{A:=?25[_ ; _]})
+### (* REDUCED disambiguated term *)
+nil{A:=?25[_ ; _]}