NCic.context -> NCic.term -> int ->
NCic.term * NCic.metasenv * NCic.term list
+val pack_lc : int * NCic.lc_kind -> int * NCic.lc_kind
+
val is_out_scope_tag : NCic.meta_attrs -> bool
val int_of_out_scope_tag : NCic.meta_attrs -> int
+
+val is_flexible : NCic.context -> subst:NCic.substitution -> NCic.term -> bool