{α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LE α] →
      {motive : Std.PRange.LawfulUpwardEnumerableLE α → Sort u_1} →
        (t : Std.PRange.LawfulUpwardEnumerableLE α) →
          ((le_iff : ∀ (a b : α), a ≤ b ↔ Std.PRange.UpwardEnumerable.LE a b) → motive ⋯) → motive t