diff --git a/algebra/upred.v b/algebra/upred.v
index 5e0cf611a9ca212a47c85cec2a62290226986de0..659af0b655b452e9bf5913a509c753b8b7f5c430 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -747,6 +747,13 @@ Proof.
 Qed.
 Lemma wand_diag P : (P -★ P)%I ≡ True%I.
 Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed.
+Lemma wand_entails P Q : True ⊑ (P -★ Q) → P ⊑ Q.
+Proof.
+  intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r.
+Qed.
+Lemma entails_wand P Q : (P ⊑ Q) → True ⊑ (P -★ Q).
+Proof. auto using wand_intro_l. Qed.
+
 Lemma sep_and P Q : (P ★ Q) ⊑ (P ∧ Q).
 Proof. auto. Qed.
 Lemma impl_wand P Q : (P → Q) ⊑ (P -★ Q).
diff --git a/barrier/proof.v b/barrier/proof.v
index 4e128f74c07f9c6d5610f2ac2a003ed1037a6a1c..c6b4caff4d7fa422e43b5191282c0105e4a50779 100644
--- a/barrier/proof.v
+++ b/barrier/proof.v
@@ -332,4 +332,11 @@ Proof.
   rewrite (later_intro (P1 -★ _)%I) -later_sep. apply later_mono.
   apply wand_intro_l. by rewrite !assoc wand_elim_r wand_elim_r.
 Qed.
+
+Lemma recv_mono l P1 P2 :
+  P1 ⊑ P2 → recv l P1 ⊑ recv l P2.
+Proof.
+  intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_strengthen.
+Qed.
+
 End proof.
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 1ec0f937d281c2dac85bf25adc51902416d59f72..f79f159762bed09cb0e798024e5d656e0ab59772 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -78,3 +78,11 @@ Notation "'rec:' f x y z := e" := (Rec f x (Lam y (Lam z e%L)))
   (at level 102, f, x, y, z at level 1, e at level 200) : lang_scope.
 Notation "'rec:' f x y z := e" := (RecV f x (Lam y (Lam z e%L)))
   (at level 102, f, x, y, z at level 1, e at level 200) : lang_scope.
+Notation "λ: x y , e" := (Lam x (Lam y e%L))
+  (at level 102, x, y at level 1, e at level 200) : lang_scope.
+Notation "λ: x y , e" := (LamV x (Lam y e%L))
+  (at level 102, x, y at level 1, e at level 200) : lang_scope.
+Notation "λ: x y z , e" := (Lam x (LamV y (LamV z e%L)))
+  (at level 102, x, y, z at level 1, e at level 200) : lang_scope.
+Notation "λ: x y z , e" := (LamV x (LamV y (LamV z e%L)))
+  (at level 102, x, y, z at level 1, e at level 200) : lang_scope.