Lemmas which are consequences of monoidal coherence #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
These lemmas are all proved
Future work #
Investigate whether these lemmas are really needed,
or if they can be replaced by use of the