+(* Note: maps only variables <= freshno *)
+let env_of_sigma freshno sigma =
+ let rec aux n =
+ if n > freshno then
+ []
+ else
+ let e = aux (n+1) in
+ (try
+ e, lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[]
+ with
+ Not_found -> ([], V n, []) ) :: e
+ in aux 0
+