enrich list-set with predicates . ≡ . : list × list; axioms setequal-def : ⊦ x ≡ y ↔ x ⊆ y ∧ y ⊆ x; used for: ls; end enrich