la_tautology

I still don't get the second case of this rule.

First, of all there are two cases for equality and I remember vaguely from a long time ago that one is merely a typo?

Then, the normalizations in the la_generic rule are applied (which ones?) to the binary clause \phi_1 \lor \phi_2 which results in s_1 \circ d? What is d1 and d2 and why is there no s2?

The description should be improved.