- 'a * Inference.proof *
- (Index.key * Index.key * Index.key * Utils.comparison) * Cic.metasenv * 'c ->
- int *
- (int * Inference.proof *
- (Index.key * Index.key * Index.key * Utils.comparison) * Cic.metasenv *
- 'e list)
- list
+ Equality.equality ->
+ (Subst.substitution * Equality.equality * bool) option
+
+val superposition_left :
+ Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
+ Index.t -> Equality.goal -> int ->
+ int * Equality.goal list
+