validateAccount(ident username, string code) {
  assume exists //accounts/account[username]/code; # implies existence of the account
 
  assume //accounts/account[username]/code = code;
 
  remove //accounts/account[username]/code;
}