For all big_op lemmas which had an
Absorbing condition, the condition
has now become an alternative between
Absorbing. Thus the
lemmas are made more general. This is spreading the use of the
TCOr (Affine _) (Absorbing _) pattern.
Impact on reverse dependencies needs assessment. As this MR only weakens existing TC arguments, in theory it shouldn’t cause many breakages, but experience shows that
TCOr instances are not always inferred fully automatically.