| NCic.Sort (NCic.Type _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
| NCic.Implicit _ -> assert false
| NCic.Const (NReference.Ref (u,NReference.Ind (_,i,_))) ->
| NCic.Sort (NCic.Type _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
| NCic.Implicit _ -> assert false
| NCic.Const (NReference.Ref (u,NReference.Ind (_,i,_))) ->