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

There was an error rendering this math block. KaTeX parse error: Undefined control sequence: \/ at position 8: \phi_1 \̲/̲ \phi_2

which results in

$s_1 o d$

? What is d1 and d2 and why is there no s2?

The description should be improved.

added clarification format rules todo-specification labels

assigned to @hjsc