Use reduceTyFamApp_maybe in Lint

[monoidal]

Currently Core Lint manually reduces multiplication of multiplicities in normalize inside ensureSubMult. Goal: change to reduceTyFamApp_maybe.

[aspiwack]

Maybe? Though we do want (p `MultMul` q) `MultMul` r) to normalise to the same expression as p `MultMul` (q `MultMul r). And I'm not sure we can manage this with just reduceTyFamApp_maybe, can we?

[monoidal]

It depends on how smart we want Lint to be. More complex properties such as associativity could be just axioms and Core would have coercions witnessing them.

[aspiwack]

Fair enough. I don't have strong opinion either way.