wellFounded_iff_no_descending_seq relies on StrictOrder

Stream: Is there code for X?

[Dexin Zhang]

Hello! I'm trying to prove that second-order ZF has a well-founded membership relation. This theorem looks very nice:

theorem wellFounded_iff_no_descending_seq :
    WellFounded r ↔ IsEmpty (((· > ·) : ℕ → ℕ → Prop) ↪r r)

But it relies on an instance [IsStrictOrder α r] which doesn't hold for set membership in ZF. In my understanding, a stronger version can be proved:

-- in my understanding
theorem wellFounded_iff_no_descending_seq :
    WellFounded r ↔ IsEmpty { f : ℕ → α // ∀ n : ℕ, r (f n) (f (n + 1)) }

without reliance on IsStrictOrder. Does mathlib have such a theorem? Thanks!