# Library variables

We define our variables exactly as that in Software Foundations
.
Basically, variables are wrappers around numbers.
We could have defined them as wrappers around any (countably) infinite
type with decidable equality.

Here are some examples of variables.

We need decidable equality on variables so that
many useful relations on our future definitions of Terms, like equality,
alpha equality, etc. will be decidable.
Also our substitution function will need this decidable equality to
decide whether it needs to come up with fresh variables.
Decidable equality on variables is a straightforward consequence
of decidable equality on the underlying type.

Another key requirement for a sensible formalization of variables
is to have an unbounded supply of fresh variables. Hence,
we prove the following lemma.
To those who are unfamiliar
with constructive logic, the following lemma might just
say that that for any n and lv, there exists a list lvn
of length n of distinct variables such that the members of lvn
are disjoint from the members of lv.
However, because of the propositions as types principle,
We are actually defining a function fresh_vars that takes a number
n and a list lv of variables and returns a 4-tuple.
The first member of that tuple is lvn, a list of variables with
the above mentioned properties. The next three members are proofs
of the desired properties of lvn.
An important use free_vars of it will be in defining
the substitution function.