sig
  type t = {
    carrier : Term.constr;
    eq : Term.constr;
    equivalence : Term.constr;
  }
  val make :
    Term.constr -> Term.constr -> Term.constr -> AAC_coq.Equivalence.t
  val infer :
    AAC_coq.goal_sigma ->
    Term.constr -> Term.constr -> AAC_coq.Equivalence.t * AAC_coq.goal_sigma
  val from_relation :
    AAC_coq.goal_sigma ->
    AAC_coq.Relation.t -> AAC_coq.Equivalence.t * AAC_coq.goal_sigma
  val cps_from_relation :
    AAC_coq.Relation.t ->
    (AAC_coq.Equivalence.t -> Proof_type.tactic) -> Proof_type.tactic
  val to_relation : AAC_coq.Equivalence.t -> AAC_coq.Relation.t
  val split :
    AAC_coq.Equivalence.t -> Term.constr * Term.constr * Term.constr
end