Index.t ->
Equality.goal ->
bool * Equality.goal
+val demodulation_all_goal :
+ Equality.equality_bag ->
+ Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+ Index.t ->
+ Equality.goal -> int ->
+ Equality.goal list
val demodulation_theorem :
Equality.equality_bag ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->