Fixing clausification.

This time round, examples/elf/unique.thm is actually a correct proof.