The notation {{M\[X <\- N\]}} means {{M}} with all occurrences of the symbol {{X}} replaced by the expression {{N}}.  It is very costly to actually perform these subtitutions on =norm-if-form= data.  To avoid this computational expense, we simply maintain a list of bindings which are pairs consisting of symbols (variable names) and boolean values {{{true}}, {{false}}.  The following data definition definition formally defines the {{binding}} type.