Refactor finite map/finite sets and prove map-list/set-list equality

* Pull the functionality we need into a Containers.v file that takes
  care of including the proper implementations of fmaps and fsets.
  Additionally, this file defines notation/new names.
* Stop using map/set notation for operations. This conflicts with
  lists/record-set and is generally a head-ache.
* Switch to lists instead of AVL trees for the sets and maps. This
  allows us to prove (assuming proof irrelevance) what we need:
  FSet.of_list (FSet.elements x) = x. Prove this and the equivalent for
  fin maps.
* Do not use program instances in Oak.v. We can do with instances which
  generate a lot less bloat.
3 jobs for master in 3 minutes and 13 seconds (queued for 1 second)