Documentation additions

Minor re-factorings

Added in recursive tuple simplification (to remove the need for
unnecessary generated constants)
Added in an assertion to link the subset, subseteq and length functions
Added in an assertion to define equality between tuples