fupd_plainly_laterN = fupd_plain_laterN ?
It seems fupd_plainly_laterN
is a misnamed copy of fupd_plain_laterN
. I confirmed this by giving the following proof to the existing statement:
Lemma fupd_plainly_laterN E n P `{HP : !Plain P} :
(▷^n |={E}=> P) ⊢ |={E}=> ▷^n ◇ P.
Proof. exact: fupd_plain_laterN. Qed.
I'm happy to leave the fix to anybody else.