prerr_endline "*** replace lifting -- what:";
List.iter (fun x -> prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)) what;
prerr_endline "\n*** replace lifting -- with what:";
List.iter (fun x -> prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)) with_what;
prerr_endline "\n*** replace lifting -- where:";
prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context where);
prerr_endline "*** replace lifting -- what:";
List.iter (fun x -> prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)) what;
prerr_endline "\n*** replace lifting -- with what:";
List.iter (fun x -> prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)) with_what;
prerr_endline "\n*** replace lifting -- where:";
prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context where);