Rodin HandbookThis work is sponsored by the Deploy Project This work is sponsored by the ADVANCE Project This work is licensed under a Creative Commons Attribution 3.0 Unported License 
3.2.2 SubstitutionsWe use the notation for a substitution of all free occurrences of the variable in by the expression . Several substitutions can be performed simultaneously with . In particular, we use the syntax to denote the substitution of each identifier in the sequence by . For more information on free identifiers, see Section 3.3.1.3. Examples:
