Show that step fupd commutes with forall for plain predicates in Iris.

theories/base_logic/lib/fancy_updates.v

@@ -50,6 +50,26 @@ Proof.
     iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
 Qed.
 
+Lemma step_fupd_forall_plain `{invG Σ} {A: Type} E (Ψ: A → iProp Σ) `{∀ x : A, Plain (Ψ x)}:
+  (|={E, ∅}▷=> ∀ a, Ψ a)%I ⊣⊢ (∀ a, |={E, ∅}▷=> Ψ a)%I.
+Proof.
+  intros. apply (anti_symm (⊢)).
+  - iIntros "H". iIntros (a). iMod "H".
+    iModIntro. iNext. iMod "H"; auto.
+  - rewrite uPred_fupd_eq /uPred_fupd_def.
+    iIntros "H (Hw&HE)".
+    iMod (ownE_empty) as "Hemp".
+    iAssert (▷ ◇ ∀ a, Ψ a)%I with "[Hw HE H]" as "#Hplain".
+    {
+      iIntros (a). iMod ("H" $! a with "[$Hw $HE]") as ">(Hw&HE&H)".
+      iNext. iMod ("H" with "[$Hw $HE]") as ">(?&?&$)".
+    }
+    iAssert (wsat ∗ ownE ∅ ∗ ▷ (wsat ∗ ownE ∅ ==∗ ◇ (wsat ∗ ownE E)))%I
+      with "[H Hw HE Hemp]" as "($&$&H)".
+    { iFrame. by iIntros "!> (?&?)". }
+    iIntros "!> !> !> Hw". by iMod ("H" with "Hw") as ">($&$)".
+Qed.
+
 Lemma fupd_plain_soundness `{invPreG Σ} E (P: iProp Σ) `{!Plain P}:
   (∀ `{Hinv: invG Σ}, (|={⊤, E}=> P)%I) → (▷ P)%I.
 Proof.