505   One huge advantage of using bijective permutation functions (as opposed to

   505   An \emph{equivariant} function or predicate is one that is invariant under

   506   non-bijective renaming substitutions employed in traditional works on syntax) is 

   506   the swapping of atoms.  Having a notion of equivariance with nice logical

   507   the property of \emph{equivariance}

   507   properties is a major advantage of bijective permutations over traditional

   508   and the fact that most HOL-functions (this includes constants) whose argument

   508   renaming substitutions \cite[\S2]{Pitts03}.  Equivariance can be defined

   509   and result types are permutation types satisfy this property:

   509   uniformly for all permutation types, and it is satisfied by most HOL

   510   functions and constants.