Function obeys_range_step_spec 

pub uninterp spec fn obeys_range_step_spec<A>() -> bool

Whether A’s executable stepping, comparison, and cloning obey the model used by range iterators. The axioms below establish this for primitive integers only; implementing StepSpecImpl alone does not establish it.