Library Variables


This library defines sets of variables.

Equality of variables in the set must be decidable.

Record variables : Type := Variables {
  variable :> Type;
  beq_var : variable -> variable -> bool;
  beq_var_ok : forall x y, beq_var x y = true <-> x = y
}.

Implicit Arguments Variables [variable beq_var].
Implicit Arguments beq_var [v].
Implicit Arguments beq_var_ok [v x y].