Efficient test of multiplicity-preservingness of η-reduction

[aspiwack]

In the function performing η-reduction, in Core, we implemented a very naive check that η-reduction does not change unrestricted arrows to linear arrows, which would break typing.

We ought to come up with a more efficient way to perform this test.