Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
Equality.equality ->
- (Subst.substitution * Equality.equality) option
+ (Subst.substitution * Equality.equality * bool) option
val subsumption :
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
Equality.equality ->
- (Subst.substitution * Equality.equality) option
+ (Subst.substitution * Equality.equality * bool) option
val superposition_left :
Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
Index.t ->
val superposition_right :
?subterms_only:bool ->
+ UriManager.uri ->
int ->
'a * Cic.context * CicUniv.universe_graph ->
Index.t ->
val demodulation_equality :
?from:string ->
+ UriManager.uri ->
int ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->