in
C.Var (uri,exp_named_subst')
| C.Meta (i, l1) as t ->
+(* CSC: BIG BUG HERE! In the explicit substitution l1 = [t1 ; t2], *)
+(* CSC: it is NOT true that Rel(1) in t2 refers to t1 (i.e. the explicit *)
+(* CSC: substitution is simultaneous, not telescopic. To be fixes ASAP. *)
let rec deliftl j =
function
[] -> []