Instances.S
type instances = (Expr.gformula * Explanation.t) list
val empty : t
val add_terms : t -> AltErgoLib.Expr.Set.t -> Expr.gformula -> t
val add_lemma : t -> Expr.gformula -> Explanation.t -> t
val add_predicate : t -> Expr.gformula -> Explanation.t -> t
val matching_terms_info :
t ->
Matching_types.info AltErgoLib.Expr.Map.t
* Expr.t list AltErgoLib.Expr.Map.t Symbols.Map.t