No longer need to depend on HOL theories of cardinality.
Add while loops to PseudoC.

Symbolic evaluation should work.  Theorems go through OK.  Note that
the graphOf function will return NONE for programs that include while
statements.