// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

function domain<U, V>(m: imap<U,V>): set<U>
   ensures forall i :: i in domain(m) <==> i in m;
{
   set s | s in m // UNSAFE, m may have infinite domain
}