* From now on we recreate a kernel abstraction where substitutions are part of
* the calculus *)
+val lift : Cic.metasenv -> substitution -> int -> Cic.term -> Cic.term
+
val whd: Cic.metasenv -> substitution -> Cic.context -> Cic.term -> Cic.term
val are_convertible: