equality:((string * NCic.context_entry) list ->
NCic.term -> NCic.term -> bool) ->
context:(string * NCic.context_entry) list ->
equality:((string * NCic.context_entry) list ->
NCic.term -> NCic.term -> bool) ->
context:(string * NCic.context_entry) list ->