+val solve_narrowing:
+ Equality.equality_bag ->
+ ProofEngineTypes.status ->
+ active_table ->
+ passive_table ->
+ int ->
+ (Cic.substitution *
+ ProofEngineTypes.proof *
+ ProofEngineTypes.goal list) option *
+ active_table * passive_table * Equality.equality_bag