minimize further

src/Init/Data/Range/Polymorphic/RangeIteratorTest.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Iterators.Internal.Termination
+
+public section
+
+open Std.Iterators
+
+structure RangeIterator where
+
+instance : Iterator RangeIterator Id Nat := sorry
+
+private def RangeIterator.instFinitenessRelation : FinitenessRelation RangeIterator Id where
+  rel :=
+    open Classical in
+    InvImage WellFoundedRelation.rel (fun it => 0)
+  wf := sorry
+  subrelation {it it'} h := by
+    simp_wf
+    sorry

src/Init/Data/Vector/Basic.lean

@@ -15,6 +15,7 @@ public import Init.Data.Array.Range
 public import Init.Data.Range
 import Init.Data.Slice.Array.Basic
 public import Init.Data.Stream
+import Init.Data.Range.Polymorphic.RangeIteratorTest
 
 public section