interpretation "nil" 'nil = (cic:/matita/list/list.ind#xpointer(1/1/1) _).
interpretation "cons" 'cons hd tl =
(cic:/matita/list/list.ind#xpointer(1/1/2) _ hd tl).
interpretation "nil" 'nil = (cic:/matita/list/list.ind#xpointer(1/1/1) _).
interpretation "cons" 'cons hd tl =
(cic:/matita/list/list.ind#xpointer(1/1/2) _ hd tl).