type equality =
    Cic.term *     (* proof *)
    (Cic.term *    (* type *)
     Cic.term *    (* left side *)
     Cic.term) *   (* right side *)
    Cic.metasenv * (* environment for metas *)
    Cic.term list  (* arguments *)
;;

type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;


(**
   Performs the beta expansion of the term "where" w.r.t. "what",
   i.e. returns the list of all the terms t s.t. "(t what) = where".
*)
val beta_expand:
  ?metas_ok:bool -> ?match_only:bool -> Cic.term -> Cic.term -> Cic.term ->
  Cic.context -> Cic.metasenv -> CicUniv.universe_graph ->
  (Cic.term * Cic.substitution * Cic.metasenv * CicUniv.universe_graph) list

    
(**
   scans the context to find all Declarations "left = right"; returns a
   list of tuples (proof, (type, left, right), newmetas). Uses
   PrimitiveTactics.new_metasenv_for_apply to replace bound variables with
   fresh metas...
*)
val find_equalities:
  ?eq_uri:UriManager.uri -> Cic.context -> ProofEngineTypes.proof ->
  equality list * int


exception TermIsNotAnEquality;;

(**
   raises TermIsNotAnEquality if term is not an equation.
   The first Cic.term is a proof of the equation
*)
val equality_of_term: ?eq_uri:UriManager.uri -> Cic.term -> Cic.term ->
  equality

(**
   superposition_left env target source
   returns a list of new clauses inferred with a left superposition step
   the negative equation "target" and the positive equation "source"
*)
val superposition_left: environment -> equality -> equality -> equality list

(**
   superposition_right newmeta env target source
   returns a list of new clauses inferred with a right superposition step
   the positive equations "target" and "source"
   "newmeta" is the first free meta index, i.e. the first number above the
   highest meta index: its updated value is also returned
*)
val superposition_right:
  int -> environment -> equality -> equality -> int * equality list

val demodulation: int -> environment -> equality -> equality -> int * equality

val meta_convertibility_eq: equality -> equality -> bool

val is_identity: environment -> equality -> bool

val string_of_equality: ?env:environment -> equality -> string