match (R.whd context ty) with
(C.MutInd (uri, typeno, exp_named_subst))
| (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) ->
match (R.whd context ty) with
(C.MutInd (uri, typeno, exp_named_subst))
| (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) ->