nil : set
  add : t * set -> set

There are no equations between the lists you build up using nil and
add, aside from reflexivity.  A finite set is also generated by these
two function symbols, but it satisfies the two additional equations

  forall x, y, rest. add x (add y rest) == (add y (add x rest))

and

  forall x, rest. add x (add x rest) == add x rest

The first equation says that changing the order of insertion doesn't
change the value, and the second says that adding the same element
multiple times won't change the value. (The second equation is why
sets require equality.)

Assuming that you have a function

  choose : set -> (t * set) option

which satisfies the equations

  choose nil == None

and

  forall x, rest. there exist x', rest'.
    (add x rest) == (add x' rest') and
    (x' not in rest') and
    choose (add x rest) == Some(x', rest')

then you can define a perfectly good map function in the obvious way:

  fun map f list =
    case choose list of
      None => nil
    | Some(x', rest') => add x' (map f rest')

Now, you can show the correctness of map with a simple inductive
argument based on the number of distinct elements of a finite
set. There are other ways of specifying sets algebraically, but this
works fine -- you can define map, union, and so on, and relatively
easily prove that they have the desired properties.

If I understand you correctly, the reason you're worried arises from
something like the following implementation:

  structure IntSet =
  struct
    type set = int list

    val nil = []

    val add (x, set) = x :: set

    fun choose [] = NONE
      | choose (x :: tail) = SOME(x, filter (fn x' => x <> x') tail)
  end

You are worried that if you have

val s = add(1, add(2, nil))
val r = add(2, add(1, nil))

then s and r represent the same set {1,2}, but that calls to s and
r can give different results:

  choose(s) evaluates to SOME(1, {2})

and

  choose(r) evaluates to SOME(2, {1})

This superficially looks like it breaks the equational reasoning
property. However, this isn't actually so, because of the way that we
specified choose:

  forall x, rest. there exist x', rest'.
    (add x rest) == (add x' rest') and
    (x' not in rest') and
    choose (add x rest) == Some(x', rest')

Here, we very carefully DON'T say that

  choose (add x rest) == Some(x, rest)

Instead, we use an existential quantifier to say that choose returns
some distinct element of the set, not necessarily the "most recently
inserted" one. Indeed, upon reflection it should be clear that because
of the property that the order of insertion doesn't matter, we /can't/
promise any such behavior.