diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index 67ca47e2b299b191fe14931276ca22abae998743..f6bd2c4468f913328daaea5dfb6918eae8adbfed 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -678,10 +678,8 @@ let rec flatten_sequence m = function
 (* --- Mapping                                                            --- *)
 (* -------------------------------------------------------------------------- *)
 
-let lift f e = F.e_prop (f (F.p_bool e))
-
 let rec map_condition f = function
-  | State s -> State (Mstate.apply (lift f) s)
+  | State s -> State (Mstate.apply (F.p_lift f) s)
   | Have p -> Have (f p)
   | Type p -> Type (f p)
   | When p -> When (f p)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 8dcfa782c14e65b50f3a291f06a15ed886a57950..a75ac05e65cba2e5466a73ce9eebcdeeddaaa5ac 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -783,7 +783,8 @@ struct
   let e_prop t = t
   let p_bools xs = xs
   let e_props xs = xs
-  let lift f x = f x
+  let e_lift f = f
+  let p_lift f = f
 
   let is_zero e = match QED.repr e with
     | Kint z -> Integer.equal z Integer.zero
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index b78d557b1d0e4be9f3d1fef10f87b63a1b7aee24..c685aeaaca38508b78ff5c42a2cb33fd615b9936 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -356,7 +356,8 @@ sig
   val e_prop : pred -> term
   val p_bools : term list -> pred list
   val e_props : pred list -> term list
-  val lift : (term -> term) -> pred -> pred
+  val e_lift : (term -> term) -> pred -> pred
+  val p_lift : (pred -> pred) -> term -> term
 
   val p_not : pred -> pred
   val p_and : pred -> pred -> pred