Relaxing equiv

[alxest]

df29abd
It turns out the proof becomes quite annoying; let's do this when it is definitely needed.

[alxest]

The use case I had in my mind:
I would like to understand Sk.t as a resource, whose type is list ident but morally it means just a set.
If we define add := app, commutativity/associativity doesn't hold.

Workaround:
(1) use sort after add in order to get one canonical form (?)
(2) use multiset (ident -> nat) instead of list ident

[alxest]

I think (2) approach won't work.
I want load_mem, load_skenv to be functions, so that we can execute it, and with (2) we can't.

Let's not bother making Sk.t as a resource; unless there is concrete advantage.