List of theorems referencing the symbol ENUM_ORD

(68+) Theorem 47: [Enumeration single-valuedness principle] (FORALL s | (Ord(enum_Ord(s)) & (s = {enum(y,s): y in enum_Ord(s)}) & (FORALL y in enum_Ord(s), z0 in enum_Ord(s) | ((y /= z0) •imp (enum(y,s) /= enum(z0,s))))))