val demodulation_theorem :
'a ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
Cic.term * Index.key * Cic.metasenv ->
'a * (Cic.term * Index.key * Cic.metasenv)
val demodulation_theorem :
'a ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
Cic.term * Index.key * Cic.metasenv ->
'a * (Cic.term * Index.key * Cic.metasenv)