| (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
+alias id cons = cic:/CoRN/algebra/ListType/list.ind#xpointer(1/1/2)
+alias id list = cic:/CoRN/algebra/ListType/list.ind#xpointer(1/1)
+alias id nil = cic:/CoRN/algebra/ListType/list.ind#xpointer(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)
+ 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[_ ; _]})
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
+alias id cons = cic:/Coq/Lists/List/list.ind#xpointer(1/1/2)
+alias id list = cic:/Coq/Lists/List/list.ind#xpointer(1/1)
+alias id nil = cic:/Coq/Lists/List/list.ind#xpointer(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)
+ 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[_ ; _]})
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
+alias id cons = cic:/Coq/Lists/MonoList/list.ind#xpointer(1/1/2)
+alias id list = cic:/Coq/Lists/MonoList/list.ind#xpointer(1/1)
+alias id nil = cic:/Coq/Lists/MonoList/list.ind#xpointer(1/1/1)
### (* METASENV after disambiguation *)
### (* TERM after disambiguation *)
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
+alias id cons = cic:/Lannion/continuations/weight/specif/list.ind#xpointer(1/1/2)
+alias id list = cic:/Lannion/continuations/weight/specif/list.ind#xpointer(1/1)
+alias id nil = cic:/Lannion/continuations/weight/specif/list.ind#xpointer(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)
+ 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[_ ; _]})