With large proof contexts and lemmas with many forall quantifiers,
iIntoEmpValid can become quite slow. This makes it go faster by adding
"fast paths" for the -> and forall cases, gated by Ltac pattern
matching (which is faster than trying to unify with refine and fail).

In 13c5c1ad I strengthened bi.persistent_sep_dup
to support propositions that are persistent and either affine or absorbing; do
the same for `persistent_fractional`.