diff --git a/theories/bi/derived_laws_later.v b/theories/bi/derived_laws_later.v
index 06084c0be2d41a6ab1a7bf6abd5bc8f948916fac..a683467de724d154d0e9fc20e20c22eba4df1cec 100644
--- a/theories/bi/derived_laws_later.v
+++ b/theories/bi/derived_laws_later.v
@@ -165,6 +165,12 @@ Proof.
   by rewrite -later_and impl_elim_r (comm _ R) wand_elim_r.
 Qed.
 
+(** A funny consequence of Löb induction.
+This shows that Löb induction is incompatible with classical logic.
+See [lib/counterexamples.v] for a fully worked-out proof of that fact. *)
+Lemma not_not_later_False `{!BiLöb PROP} : ⊢@{PROP} ¬ ¬ ▷ False.
+Proof. apply entails_impl, löb. Qed.
+
 (* Iterated later modality *)
 Global Instance laterN_ne m : NonExpansive (@bi_laterN PROP m).
 Proof. induction m; simpl. by intros ???. solve_proper. Qed.