Inductive access : Set :=
  | AccessAllowed
  | AccessDenied
  .
