The results in this section are mostly meant for being used by automatic proof building programs. As a result, they might appear less useful or meaningful than others to human beings.