diff --git a/theories/lifetime/rebor.v b/theories/lifetime/rebor.v
index 3dabd333266300f9dd66e4879bfa386cee923740..5311c81dd034041899bd594dcb488e3c14295b0b 100644
--- a/theories/lifetime/rebor.v
+++ b/theories/lifetime/rebor.v
@@ -4,10 +4,6 @@ From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
 
-Global Instance into_wand_bupd {M} (R P Q : uPred M) :
-  IntoWand R P Q → IntoWand R (▷ P) (▷ Q) | 100.
-Proof. rewrite /IntoWand=>->. Admitted.
-
 Section rebor.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.