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