For all big_op lemmas which had an `Absorbing` condition, the condition
has now become an alternative between `Affine` and `Absorbing`. Thus the
lemmas are made more general. This change is spreading the use of the
`TCOr (Affine _) (Absorbing _)` pattern.

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