Feature Request: Set of queries / a way of talking about subcaches

[BoltonBailey]

In the course of working with merkle trees, it has started to seem like it might be convenient to talk about concepts like "the set of query-response pairs associated with a particular QueryCache state". It would be nice to have a definition like this:

/--
Returns, for a particular oracle's cache,
the set of all (query, response) pairs that have been made to the oracle.
-/
def QueryCache.toSet {ι : Type} {spec : OracleSpec ι} (i : ι) (cache : spec.QueryCache) :
    Set (spec.domain i × spec.range i) :=
  { (q, r) : spec.domain i × spec.range i | cache i q = some r }

and associated API.

---

Alternatively, it might be nice if we could just have some way of reasoning about subcaches and supercaches, like a HasSubset instance.