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 ->