No longer use wp_cwp_bind.

theories/c_translation/monad.v

@@ -118,11 +118,6 @@ Section cwp_rules.
     CWP fill K e @ R {{ Φ }}.
   Proof. rewrite cwp_eq. by apply: wp_bind. Qed.
 
-  Lemma wp_cwp_bind_inv R Φ K e :
-    CWP fill K e @ R {{ Φ }} -∗
-    WP e {{ v, CWP fill K (of_val v) @ R {{ Φ }} }}.
-  Proof. rewrite cwp_eq. by apply: wp_bind_inv. Qed.
-
   Lemma cwp_insert_res e Φ R1 R2 :
     ▷ R1 -∗
     CWP e @ (R1 ∗ R2) {{ v, ▷ R1 ={⊤}=∗ Φ v }} -∗
@@ -184,10 +179,7 @@ Section cwp_rules.
     φ →
     ▷^n CWP (fill K e2) @ R {{ Φ }} -∗
     CWP (fill K e1) @ R {{ Φ }}.
-  Proof.
-    iIntros (? Hφ) "Hcwp". iApply wp_cwp_bind. wp_pure _.
-    by iApply wp_cwp_bind_inv.
-  Qed.
+  Proof. iIntros (? Hφ) "Hcwp". rewrite cwp_eq /cwp_def. by wp_pure _. Qed.
 
   Lemma cwp_ret e R Φ :
     WP e {{ Φ }} -∗ CWP c_ret e @ R {{ Φ }}.