ch:hol: theorem-constructor side conditions

Problem and invariant. The tiny equality fragment records assumptions and a conclusion. Implement free occurrence, lift it to assumption lists, and let abstraction return a theorem only when its variable is absent from every assumption.

Build and mutation. Add reflexivity and a derived symmetry operation. From assumption x = c, abstraction over a different variable succeeds, while abstraction over x returns None. Deleting the traversal changes the latter oracle.

Acceptance and boundary. Require four passes and an empty audit under the appendix E commands. The corpus exposes the side condition; it neither expands every production-kernel inference nor proves HOL soundness.