unify:(NCic.metasenv -> NCic.substitution -> NCic.context ->
NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) ->
NCic.metasenv -> NCic.substitution -> NCic.context ->
unify:(NCic.metasenv -> NCic.substitution -> NCic.context ->
NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) ->
NCic.metasenv -> NCic.substitution -> NCic.context ->