state ->
(NCic.term * NCic.term) ->
(NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
+val demod :
+ #NRstatus.status ->
+ NCic.metasenv -> NCic.substitution -> NCic.context ->
+ state ->
+ (NCic.term * NCic.term) ->
+ (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list