enrich list-prefixn, set-union with functions . .toSet : list → set; axioms toSet-ext : ⊦ a ∈ x.toSet ↔ a ∈ x; used for: s, ls; end enrich