let status, kind = match ty with
| NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;_;l;r]
when NUri.name_of_uri u = "eq" ->
classify ~subst:(get_subst status) ctx_ty l r
| NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;lty;l;rty;r]
when NUri.name_of_uri u = "jmeq" &&
let status, kind = match ty with
| NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;_;l;r]
when NUri.name_of_uri u = "eq" ->
classify ~subst:(get_subst status) ctx_ty l r
| NCic.Appl [NCic.Const (NReference.Ref (u,_)) ;lty;l;rty;r]
when NUri.name_of_uri u = "jmeq" &&