Adding identity-related formation and inference rules (two of each)

On p. 134, Grice extends his natural deduction system to cover the 'atomic' (not molecular) identity formula:

a = b

---

For which he adds to the previous one two formation rules:

1. for w1=n w2 is a formula
2. If aj+k =j bj+i is a formula, aj+k=mbetaj+i is a formula, where m>j+k and m>k+l.

---

The two inference rules which are added read:

1. (=, +):

Gamma /- Awn+mwn-l =n wn-l ('weak identity law')

2. (=, -).

aj=m betak, phi /- phi (beta/alpha)

(substitutivity on both strong and weak identity).