∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α] {it : Std.Iter α}
  {step : Std.IterStep (Std.Iter α) α}, it.IsPlausibleStep step ↔ step = Std.Rxo.Iterator.step it