(* order (in the sense of alpha-conversion). See comment above *)
(* related to the delift function. *)
debug_print "\n!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
-print_endline "\nCicMetaSubst: UNCERTAIN" ;
+debug_print "\nCicMetaSubst: UNCERTAIN" ;
raise (Uncertain (sprintf
"Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
(ppterm subst t)