val forward_infer_step:
#NCic.status -> NCic.metasenv -> NCic.substitution -> NCic.context ->
state -> NCic.term -> NCic.term -> state
val forward_infer_step:
#NCic.status -> NCic.metasenv -> NCic.substitution -> NCic.context ->
state -> NCic.term -> NCic.term -> state