diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index fa6e17a4ddec2150f394086d0898031297e621f6..3f909e5b7b0042e96e4652606a4dae3627bc4203 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -1975,11 +1975,11 @@ struct
 
   let let_intro_case q x a =
     let res = ref None in
+    let found_term t = assert (!res = None);
+      assert (not (Vars.mem x t.vars));
+      res := Some t; true
+    in
     let is_term_ok a b =
-      let found_term t = assert (!res = None);
-        assert (not (Vars.mem x t.vars));
-        res := Some t; true
-      in
       match a.repr with
       | Fvar w -> assert (Var.equal x w); found_term b
       | Add e ->
@@ -2010,8 +2010,16 @@ struct
       | false,true -> is_term_ok v u
       | _,_ -> false
     in
-    let is_eq e  = match e.repr with|Eq(u,v) -> is_var_ok u v |_ -> false in
-    let is_neq e = match e.repr with|Neq(u,v)-> is_var_ok u v |_ -> false in
+    let is_boolean_var polarity_term = function
+      | Fvar w when Var.equal x w -> found_term polarity_term
+      | _ -> false
+    in
+    let is_eq e = match e.repr with | Eq(u,v) -> is_var_ok u v
+                                    | Not q -> is_boolean_var e_false q.repr
+                                    | rep -> is_boolean_var e_true rep in
+    let is_neq e = match e.repr with | Neq(u,v)-> is_var_ok u v
+                                     | Not q -> is_boolean_var e_true q.repr
+                                     | rep -> is_boolean_var e_false rep in
     match q with
     | Lambda -> None
     | Forall ->
diff --git a/src/plugins/wp/tests/wp_bts/ex5.i b/src/plugins/wp/tests/wp_bts/ex5.i
index 5a4b45fe866708383e7af25b0989bab1e3df2f87..af1e3e63c0a03a4ad51c5caae8a7264c215ecf35 100644
--- a/src/plugins/wp/tests/wp_bts/ex5.i
+++ b/src/plugins/wp/tests/wp_bts/ex5.i
@@ -15,6 +15,10 @@ void dummy()
     predicate P(integer x) reads \nothing;
     predicate Q(integer x) reads \nothing ;
     logic integer f(integer x) reads \nothing;
+
+    predicate B(boolean x) reads \nothing;
+    predicate C(boolean x,boolean y) reads \nothing ;
+    logic boolean c(boolean x) reads \nothing;
     }
 */
 
@@ -36,6 +40,11 @@ void dummy()
     ensures p1:  \exists integer x; P(x) && Q(x) &&        x == 1;
     ensures p2:  \exists integer x; P(x) && Q(x) &&      1+x == b;
     ensures p3:  \exists integer x; P(x) && Q(x) && 1+x+f(a) == b+f(b);
+
+    ensures ok41: \exists boolean x; x && c(x) == c(\true);
+    ensures ok42: \exists boolean x; !x && c(x) == c(\false);
+    ensures ok43: \exists boolean x; \exists boolean y; !x && y && (C(x,y) <==> C(\false,\true)) ;
+    ensures ko43: \exists boolean x; \exists boolean y; !x && y && C(x,y) ;
  */
 void exists (int a, int b) {
 }
diff --git a/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle
index b20145478344b5e93bbd859c69e5a5a79e93fff4..5a458b3a95b83aae2ac64edb8ca45fe8b5143bc8 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle
@@ -99,6 +99,26 @@ Let x = b - 1. Prove: P_P(x) /\ P_Q(x).
 Goal Post-condition 'p3' in 'exists':
 Let x = b + L_f(b) - 1 - L_f(a). Prove: P_P(x) /\ P_Q(x).
 
+------------------------------------------------------------
+
+Goal Post-condition 'ok41' in 'exists':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition 'ok42' in 'exists':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition 'ok43' in 'exists':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition 'ko43' in 'exists':
+Prove: P_C(false, true).
+
 ------------------------------------------------------------
 ------------------------------------------------------------
   Function forall