diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 36313df6ce8c335fec3e9480f643ee537fb4048a..bbe2a59b3bd1d5bfe9bb5b74e68354638150bac0 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -914,9 +914,8 @@ class visitor (ctx:context) c =
                 let t = share cnv Prop (Lang.F.e_prop p) in
                 let t =
                   Why3.Term.t_forall_close vars []
-                    (Why3.Term.t_equ
-                       (Why3.Term.t_app id (List.map Why3.Term.t_var vars) result)
-                       t)
+                    (Why3.Term.t_implies t
+                       (Why3.Term.t_app id (List.map Why3.Term.t_var vars) result))
                 in
                 let decl =
                   Why3.Decl.create_prop_decl Why3.Decl.Paxiom