- | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Sort _
- | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Meta (_,(_,(C.Irl 0 | C.Ctx [])))
- | C.Sort _, C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> t2
+ | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Sort _ -> t2
+ | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Meta (i,(_,(C.Irl 0 | C.Ctx [])))
+ | C.Sort _, C.Meta (i,(_,(C.Irl 0 | C.Ctx []))) ->
+ NCic.Meta (i,(0, C.Irl 0))