| NCic.Appl (NCic.Const (NReference.Ref (u,_))::ty::_)
when NUri.string_of_uri u = "cic:/matita/tests/hole.con" ->
let metasenv, ty = perforate ctx metasenv ty in
| NCic.Appl (NCic.Const (NReference.Ref (u,_))::ty::_)
when NUri.string_of_uri u = "cic:/matita/tests/hole.con" ->
let metasenv, ty = perforate ctx metasenv ty in