todo about generalisation
formatting for readability
better documentation
labeled for reuse
rewrote Sledgehammer output for readability
rewrote Sledgehammer output for readability
not unfolding x'_def yet, to improve readability
more documentation
not unfolding x'_def yet, to improve readability
more documentation
better documentation
now unfolding x'_def
proved some of the easier remaining steps of wd_outcome
Trying to prove something that might be a dead end.  We have something like "c = a + b" but a is undefined.