metasenv:NCic.metasenv -> subst:NCic.substitution ->
NCic.context -> NCic.term -> NCic.term list -> bool list
(* type_of_branch subst context leftno outtype
* (constr @ lefts) (ty_constr @ lefts) *)
val type_of_branch :
metasenv:NCic.metasenv -> subst:NCic.substitution ->
NCic.context -> NCic.term -> NCic.term list -> bool list
(* type_of_branch subst context leftno outtype
* (constr @ lefts) (ty_constr @ lefts) *)
val type_of_branch :