[\lambda x:list. list]
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#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)
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#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)
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#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      *)

<[x:list]list>Cases nil of 
 nil => nil
 cons => [x:A][y:list](cons x y)
end
### (* TYPE_OF the disambiguated term *)
([x:list]list nil)
### (* REDUCED disambiguated term     *)
nil
###### INTERPRETATION NUMBER 4 ######
### (* disambiguation environment  *)
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)
end
### (* TYPE_OF the disambiguated term *)
([x:list{A:=?25[_ ; _]}]list{A:=?25[_ ; _]} nil{A:=?25[_ ; _]})
### (* REDUCED disambiguated term     *)
nil{A:=?25[_ ; _]}