op Find(r:Rolodex, n:Name)->(cl:CardList)
    post:
        (* Cards in the output list consist of those
         * in the input Rolodex with the given name *)
        forall (c:Card)
            (c in cl) iff ((c in r) and (c.name = n));
end;

obj CardList =  Card*;