exception Free
exception OccurCheck
+val delift :
+ Cic.context -> Cic.metasenv -> (Cic.term option) list -> Cic.term -> Cic.term * Cic.metasenv
+
(* The entry (i,t) in a substitution means that *)
(* (META i) have been instantiated with t. *)
type substitution = (int * Cic.term) list