∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] {r : Std.Rci α} {a : α},
  (Std.Rci.Internal.iter r).IsPlausibleIndirectOutput a ↔ a ∈ r