affeq: Fix array OOB in invariant

[michael-schwarz]

During benchmarking for #1297, it became apparent that the invariant function in affeq accesses arrays out-of-bounds due to an off-by-one error.

This fixes the issue and adds a test that has witness generation enabled to spot regressions.

[sim642]

Seems right, although the entire invariant is very roundabout: Matrix → earray → array → Enum → list. A single List.init should do it.