Abstract bidirectional map for layouts

[khieta]

To describe a physical-to-logical qubit association for circuit mapping, we use an ad hoc pair of a nat -> nat map and its inverse (see the layout type in Layouts.v). It would be cleaner (and easier for proof) to provide an abstract BiMap type along the lines of Coq's FMap.