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`.

Include workaround for Coq bug #14441, and drop now-failing test for that Coq
bug.

Suggestion from Gregory Malecha, forall lemmas suggested by Robbert & Ralf,
proof scripts from me.

Example include Equiv, Dist, Op, Core, Valid, ValidN and Unit.

The previous hints used eapply. The new hint now use refine. These two
tactic use a different unification algorithm, which result in
different behavior with respect to canonical structures.

The refine tactic is followed by shelving all the remaining goals,
which correspond actually to existential variables.

In particular, in RustHornBelt, the version using apply is unable to
find the canonical structure of heterogeneous lists.

also add `wand_entails'`, which was used in some earlier version of these proofs