diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index a9eaff530f4ab8081b0f02094ee3cba649c9a1e3..f1715632709a98aeb7d51e5369565efba3ed3108 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -5,6 +5,40 @@ From iris Require Import options.
 (* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
 Set Default Proof Using "Type*".
 
+(** This proves that the combination of affinity [P ∗ Q ⊢ P] and the classical
+excluded-middle [P ∨ ¬P] axiom makes the separation conjunction trivial, i.e.,
+it gives [P -∗ P ∗ P]. *)
+Module affine_em. Section affine_em.
+  Context `{!BiAffine PROP}.
+  Context (em : ∀ P : PROP, ⊢ P ∨ ¬P).
+  Implicit Types P Q : PROP.
+
+  Lemma and_sep P Q : P ∧ Q -∗ P ∗ Q.
+  Proof using All.
+    iIntros "HPQ". iDestruct (em P) as "[HP|HnotP]".
+    - iFrame "HP". by iDestruct "HPQ" as "[_ HQ]".
+    - iExFalso. iApply "HnotP". by iDestruct "HPQ" as "[HP _]".
+  Qed.
+  Lemma sep_trivial P : P -∗ P ∗ P.
+  Proof using All. iIntros "HP". iApply and_sep; auto. Qed.
+End affine_em. End affine_em.
+
+(** This proves that the combination of Löb induction [(▷ P → P) ⊢ P] and the
+classical excluded-middle [P ∨ ¬P] axiom makes the later operator trivial, i.e.,
+it gives [â–· False]. *)
+Module löb_em. Section löb_em.
+  Context `{!BiLöb PROP}.
+  Context (em : ∀ P : PROP, ⊢ P ∨ ¬P).
+  Implicit Types P : PROP.
+
+  Lemma later_False : ⊢@{PROP} ▷ False.
+  Proof.
+    iDestruct (em (â–· False)%I) as "#[HP|HnotP]".
+    - done.
+    - iExFalso. iLöb as "IH". iSpecialize ("HnotP" with "IH"). done.
+  Qed.
+End löb_em. End löb_em.
+
 (** This proves that we need the â–· in a "Saved Proposition" construction with
 name-dependent allocation. *)
 Module savedprop. Section savedprop.