Variant of Steel for_loop with a selector invariant

[R1kM]

trafficstars

This PR adds a new variant of the Steel for_loop combinator called for_loop_full, which supports the additional use of a selector invariant on top of the current vprop invariant. Note, the old for_loop combinator can now be implemented simply by calling for_loop_full'

This PR should be merged in conjunction with https://github.com/FStarLang/karamel/pull/289 , which adds support in karamel for this new combinator.