Definition 5.3. Let T be a set. We define:
Rewr(T) :=: {l → r | l, r ∈ T}
(l → r) = (l' → r') :⇔ l = l' and r = r' (l, r ∈ T, l', r' ∈ T)
For T' ⊆ T, we canonically treat elements of Rewr(T') as elements of Rewr(T).
Remarks.
This definition just provides some useful notation for rewriting rules for terms in T. It is actually equivalent to the Cartesian product of T with itself.