val equality_of_term: ?eq_uri:UriManager.uri -> Cic.term -> Cic.term ->
equality
+val term_is_equality: ?eq_uri:UriManager.uri -> Cic.term -> bool
+
(**
superposition_left env target source
returns a list of new clauses inferred with a left superposition step
val build_proof_term: equality -> Cic.term
val find_library_equalities:
- dbd:Mysql.dbd -> ProofEngineTypes.status -> int -> equality list * int
+ dbd:Mysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
+ equality list * int