iLöb doesn't work in the empty context.

As witnessed by the following example.

From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type*".

Definition assert : val :=
  λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.

Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
  WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗ WP assert: e @ E {{ Φ }}.
Proof.
  Fail (iLöb as "IH" forall (e Closed0)).
  iAssert (True)%I as "T"; [by admit|].
  (iLöb as "IH" forall (e Closed0)).
Abort.

I guess with the new unified handling of reverting hypotheses this probably applies to other tactics as well.