NCic.metasenv -> NCic.substitution -> NCic.context ->
NCic.term -> NCic.term ->
(NCic.metasenv *
(NCic.term * NCic.term) * (NCic.term * NCic.term) list) list
NCic.metasenv -> NCic.substitution -> NCic.context ->
NCic.term -> NCic.term ->
(NCic.metasenv *
(NCic.term * NCic.term) * (NCic.term * NCic.term) list) list