operation Add(r:Rolodex, c:Card)->(r':Rolodex)
    precondition: 
        (* There is no card in the input Rolodex with the same Id
         * as the given input card. *)
        (*not (exists (c' in r) c'.id = c.id);*)
	(*exists (c' in r) true;*)
	forall (c' in r) true;

    postcondition: (* Same as above *);
end Add;