Incorrect spans on loop invariant

[Lysxia]

The two spans here are wrong (they point to the first invariant instead of the 6th and 7th)

creusot/creusot/tests/should_succeed/heapsort_generic.coma

Lines 502 to 507 in 4cb864f

	{[@expl:loop invariant #6] [%#sheapsort_generic1] let c = 2 * UIntSize.to_int i + 1 in c < UIntSize.to_int end'
	/\ UIntSize.to_int start <= parent'0 (UIntSize.to_int i)
	-> le_log'0 (Seq.get (deep_model'0 v) c) (Seq.get (deep_model'0 v) (parent'0 (parent'0 c)))}
	{[@expl:loop invariant #7] [%#sheapsort_generic1] let c = 2 * UIntSize.to_int i + 2 in c < UIntSize.to_int end'
	/\ UIntSize.to_int start <= parent'0 (UIntSize.to_int i)
	-> le_log'0 (Seq.get (deep_model'0 v) c) (Seq.get (deep_model'0 v) (parent'0 (parent'0 c)))}