iIntros fails to introduce Coq-level and Iris-level universal quantifiers at once
See for example https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/ca917d76e1318fb3a6e0aa0c61f777a2e62ac8d0#51956c642cbeef54a2f1728f704193c7e23720f3_97_98: iIntros (HTsat HEsat). iIntros (tid qE) "#LFT HE HL HC".
works but iIntros (HTsat HEsat tid qE) "#LFT HE HL HC".
does not.