This module contains an advanced GetElem tactic extension for polymorphic ranges. While Init.Data.Range.Polymorphic.Basic already defines one, it only works in very basic cases where the open upper bound of the range is exactly the size of the collection.

This tactic is using omega to be more powerful, but it needs special handling for Vector, which is impossible in Init.Data.Range.Polymorphic.Basic for bootstrapping reasons.