diff --git a/bedrock2 b/bedrock2
index c0efbad8..6faf7a0e 160000
--- a/bedrock2
+++ b/bedrock2
@@ -1 +1 @@
-Subproject commit c0efbad89b8fe3a9fe3d896e901505a2d804280c
+Subproject commit 6faf7a0e064aab66feb1e32e44e5d2a901adc01e
diff --git a/src/Rupicola/Examples/CapitalizeThird/Properties.v b/src/Rupicola/Examples/CapitalizeThird/Properties.v
index b1d94516..1fdab987 100644
--- a/src/Rupicola/Examples/CapitalizeThird/Properties.v
+++ b/src/Rupicola/Examples/CapitalizeThird/Properties.v
@@ -297,8 +297,6 @@ Section Proofs.
                      try congruence)]
     end.
 
-  Import WP.
-
   (* TODO: try to use ProgramLogic *)
   Lemma capitalize_String_correct
         (addr : word) (s : Gallina.String) :
@@ -320,8 +318,8 @@ Section Proofs.
              (success = 1 /\ sep (String addr caps) R mem'))).
   Proof.
     cbv zeta. intros.
-    eapply mk_wp_call. 1: eassumption. 1: reflexivity.
-    eapply cmd_sound.
+    do 4 eexists. 1: eassumption. do 2 eexists. 1: reflexivity.
+    eapply sound_cmd.
 
     (* beginning of function body *)
     cbn [WeakestPrecondition.cmd WeakestPrecondition.cmd_body].
@@ -721,8 +719,8 @@ Section Proofs.
                   R mem'))).
   Proof.
     cbv zeta. intros.
-    eapply mk_wp_call. 1: eassumption. 1: reflexivity.
-    eapply cmd_sound.
+    do 4 eexists. 1: eassumption. do 2 eexists. 1: reflexivity.
+    eapply sound_cmd.
 
     (* beginning of function body *)
     cbn [WeakestPrecondition.cmd WeakestPrecondition.cmd_body].
diff --git a/src/Rupicola/Lib/Compiler.v b/src/Rupicola/Lib/Compiler.v
index 7b9524b2..c7c21af7 100644
--- a/src/Rupicola/Lib/Compiler.v
+++ b/src/Rupicola/Lib/Compiler.v
@@ -385,8 +385,7 @@ Section with_parameters.
         rewrite map.put_idemp in H0; assumption.
       - eapply WeakestPrecondition_weaken, IHcmd1; eauto;
           intros; eapply WeakestPrecondition_weaken, IHcmd2; eauto.
-      - eapply WP.WP_Impl.mk_wp_cmd. eapply WP.WP_Impl.invert_wp_cmd in H.
-        eapply refinement_while. 2: eassumption.
+      - eapply refinement_while. 2: eassumption.
         unfold refinement. intros.
         eapply sound_cmd. eapply IHcmd. eapply complete_cmd. assumption.
     Qed.
@@ -427,7 +426,7 @@ Section with_parameters.
       clear; firstorder eauto using getmany_list_map.
     Qed.
 
-    Import bedrock2.Semantics bedrock2.WP.
+    Import bedrock2.Semantics.
 
     Lemma compile_setup_WeakestPrecondition_call_first {tr mem locals}
           name argnames retvars body args functions post:
@@ -444,8 +443,8 @@ Section with_parameters.
       WeakestPrecondition.call functions name tr mem args post.
     Proof.
       intros.
-      eapply mk_wp_call. 1,2: eassumption.
-      eapply cmd_sound.
+      do 4 eexists. 1: eassumption. do 2 eexists. 1: eassumption.
+      eapply sound_cmd.
       eapply WeakestPrecondition_weaken; try eassumption.
       clear; firstorder eauto using getmany_list_map.
     Qed.