fix proof of first loop invariants