Library zoo.iris.base_logic.lib.fupd

From iris.base_logic Require Export
  lib.fancy_updates.

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

Lemma lc_fupd_elim_laterN `{inv_G : invGS Σ} n P E :
  £ n -∗
  ▷^n P ={E}=∗
  P.