diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index b623f0d4821499175398f183045d0a4378411bcc..7694c59b644f63a2fd7b9ce404600113c3e2fc78 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -10,6 +10,8 @@ Context {M : ucmraT}.
 Implicit Types P Q R : uPred M.
 
 (* FromAssumption *)
+Global Instance from_assumption_False p P : FromAssumption p False P.
+Proof. destruct p; rewrite /FromAssumption /= ?always_pure; apply False_elim. Qed.
 Global Instance from_assumption_exact p P : FromAssumption p P P.
 Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
 Global Instance from_assumption_always_l p P Q :
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 8a884b3d74d686e21b503425841a07b413ddb98c..63b55ce515bfd7d1c19e9c7a571e9ba2103d934d 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -127,3 +127,6 @@ Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
 
 Lemma demo_13 (M : ucmraT) (P : uPred M) : (|==> False) -∗ |==> P.
 Proof. iIntros. iAssert False%I with ">[-]" as "[]". done. Qed.
+
+Lemma demo_14 (M : ucmraT) (P : uPred M) : False -∗ P.
+Proof. iIntros "H". done. Qed.