(* The entry (i,t) in a substitution means that *)
(* (META i) have been instantiated with t. *)
type substitution = (int * Cic.term) list
(* The entry (i,t) in a substitution means that *)
(* (META i) have been instantiated with t. *)
type substitution = (int * Cic.term) list