Encoding CIC in XML: cooking and naming
In Coq it is possible to open a section, declare
some variables, define objects depending on them and close the
section
Once a section is closed, cooking starts: all the
variables are got rid of, the objects are parametrized w.r.t. them
and their Section Path is changed.
This is an example