K backends

Feature	activation	Java	coq	tiny
associative matching	assoc attribute	?	?	✔
commutative matching	comm attribute	?	?	✔ (no comm without assoc)
set	unique attribute?	limited to Set	?	✗
map	unique(1) attribute?	limited to Map	?	limited to Map
functions	function attribute	✔	?	✔ (via theory)
f. config access	function attribute	✗	?	✗
anywhere	anywhere attribute	✔ (limitations?)	?	✔ (just needs to be hooked)
everywhere (new-state generating function)	everywhere attribute?	✗	?	✔ (just needs to be hooked)