Fix order of the existentially quantified vars in list_nchotomy thm.

This makes the theorem conform to the pattern used by types in the
TypeBase. This theorem is stated explicitly here to override the
datatype package's choice of variable names, which make a difference
when you use Cases_on or Cases.
Implement function to prove a case-constant elimination rewrite
Remove two uses of old if-then-else syntax from the REFERENCE