Library zoo.iris.base_logic.lib.fupd

Require Export iris.base_logic.lib.fancy_updates.

Require Import zoo.prelude.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.diaframe.
Require Import zoo.options.

Lemma lcｰfupdｰelimｰlaterN `{inv۰G : invGS Σ} n P E :
  £ n -∗
  ▷^n P ={E}=∗
  P.