invariants.v 4.2 KB