Theorem wellFounded_iff_isEmpty_descending_chain

Modification history