let vty = match vty with
| C.Appl (C.MutInd (fu, fm, _) as hd :: args)
when UM.eq fu u && fm = m && List.length args = psno ->
let vty = match vty with
| C.Appl (C.MutInd (fu, fm, _) as hd :: args)
when UM.eq fu u && fm = m && List.length args = psno ->