That's probably premature optimization, but it's interesting that we
can express them by bitwise operations just on the 64 bit
representations of both literals.

For this to work, Term::name() is now encoded in the term ID.

Both operations are much more complicated than when we use only
propositional literals. Expressing them as bitwise operations could
help us using SAT solver technologies.

Added a file internal/ints.h with typedefs to replace std::uint64_t
with u64 etc.

Also fixed a few assertions that were wrongfully falsified.