(newmeta + 1, context, Cic.Meta (newmeta, irl))::
(newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
(uri,Cic.Meta(newmeta+2,irl))::l in
aux newmeta uris
(newmeta + 1, context, Cic.Meta (newmeta, irl))::
(newmeta + 2, context, Cic.Meta (newmeta + 1,irl))::metasenv',
(uri,Cic.Meta(newmeta+2,irl))::l in
aux newmeta uris