Index.t ->
Utils.equality_sign -> Equality.equality -> int * Equality.equality
val demodulation_goal :
- int ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
goal ->
- bool * int * goal
+ bool * goal
val demodulation_theorem :
'a ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->