Have the `[$]` pattern succeed if the premise is `True` or `emp`.

In the same way that `iFrame` would succeed on said goals.
2 jobs for gen_proofmode in 10 minutes and 33 seconds (queued for 2 seconds)
Status Job ID Name Coverage
  Build
passed #8595
fp-timing
build-coq.8.7.1

00:03:33

passed #8594
fp
build-coq.dev

00:10:33