Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
Inference.equality ->
- bool * Inference.substitution
+ (Inference.substitution * Inference.equality) option
val superposition_left :
int ->
Cic.conjecture list * Cic.context * CicUniv.universe_graph ->