* the timing proofs are incomplete, but should be easy to do (copy-paste)
* add some helper proofs (mostly related to filtering/removing in lists)

Requestor_t as an eqType and later instantiated as unit_eqType generated
problems to operate it as a natural number. Hence, the change.

* missing: WR-to-RD

* prove that CAS commands are preceded by an ACT with the same row with no
  other ACT or PRE command in between

* less direct proofs
* instead use general properties of the FIFO implementation

Added upper-level module for the memory, also a RT module for separating the RT part from the functional part of the bank