Hello Ted,
welcome to the TLA+ group!
I had a quick look at your module, and gather that your problems are about proving theorems using TLAPS. Did you experiment with TLC first? I hope that you didn't encounter any significant problems there — except that TLC cannot evaluate definitions such as
foo2 == CHOOSE f : f = [ n \in Nat |-> n * n ]
that involve an unbounded CHOOSE _expression_.
There are two types of problems in your examples. The first type involves reasoning about recursive functions such as factorial. As you well realized, the complication comes from the fact that recursive definitions involve CHOOSE expressions, so one must prove that the object that one chooses actually exists. For recursive function definitions, in particular over natural numbers, there is support through library modules (NaturalsInduction for functions of type [Nat -> S], WellFoundedInduction for more general cases), and there is some boilerplate that has to be inserted to get what you want. See attached module.
The second type involves reasoning about cardinality. Again, that boils down to CHOOSE etc., as you boldly tried to do manually. The library module FiniteSetTheorems is your friend here, although I realized that automation is insufficient for the kind of theorem you are trying to prove.
TLAPS is still in active development, so you are bound to run into problems like these, and we'd like to hear about them. I also realized when looking at the TLAPS documentation that the existing library modules do not seem to be mentioned anywhere on the current Web pages. You will find them in directory /usr/local/lib/tlaps in a typical installation of TLAPS, and you may have to add this directory to your Toolbox search path (Toolbox -> Preferences -> TLA+ Preferences -> TLA+ library path location) if it isn't done already (cf. the instructions in the Download section of the TLAPS Web pages). Adding a notice about these modules, and documentation about their contents, is on our to-do list for the next release.
Please feel free to ask for further help, we need feedback such as this for improving the current tool.
Best regards,
Stephan Merz