From the original rules of the type system, one can derive new rules
which change the context of definition of objects in the environment.
Because these rules correspond to elementary operations in the Coq
engine used in the discharge mechanism at the end of a section, we
state them explicitly.
Mechanism of substitution.
One rule which can be proved valid, is to replace a term c by its
value in the environment. As we defined the substitution of a term for
a variable in a term, one can define the substitution of a term for a
constant. One easily extends this substitution to contexts and
environments.
Substitution Property:
WF(E;Def(G)(c:=t:T); F)[D]
WF(E; F{c/t})[D{c/t}]
Abstraction.
One can modify the context of definition of a constant c by
abstracting a constant with respect to the last variable x of its
defining context. For doing that, we need to check that the constants
appearing in the body of the declaration do not depend on x, we need
also to modify the reference to the constant c in the environment
and context by explicitly applying this constant to the variable x.
Because of the rules for building environments and terms we know the
variable x is available at each stage where c is mentioned.
We said the judgment WF(E)[G] means that the defining contexts of
constants in E are included in G. If one abstracts or
substitutes the constants with the above rules then it may happen
that the context G is now bigger than the one needed for
defining the constants in E. Because defining contexts are growing
in E, the minimum context needed for defining the constants in E
is the same as the one for the last constant. One can consequently
derive the following property.