Reverted the patch that I'm unsure of.

On backtracking it may be necessary to propagate congruences again.
This happens if a appterm was created on a non-empty decide stack.
Although this is not possible at the moment, we want to keep it
running in case we want to add triggers later.

Ugly: checked is always true in buildCongruence.  I don't think it
is necessary when it is called from checkpoint, but I play safe for
now.