diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v index 227757d16aa8143552a16bdd71be88b25109cded..17576c1b30a11b6aba1ae5630c9822c974f25f25 100644 --- a/theories/typing/lib/rwlock/rwlock_code.v +++ b/theories/typing/lib/rwlock/rwlock_code.v @@ -246,7 +246,7 @@ Section rwlock_functions. iDestruct (monPred_objectively_elim with "Hβtok2") as "Hβtok2". iModIntro. destruct st2 as [[[]|[[ν q] n]]|]; simpl in Eqst2. - - exfalso. clear -Eqst2 Hm1. rewrite Eqst2 in Hm1. omega. + - exfalso. clear -Eqst2 Hm1. rewrite Eqst2 in Hm1. lia. - rewrite Eqst2. iDestruct "INT" as "[$ INT]". iExists (). iSplitL ""; [done|]. iIntros (t2 Ext2) "W' !>". iSplitL "". { rewrite /Q1 Eqst2. by iIntros "!> $". } iIntros "!> !>".