Add specialized associative List folds

[joehendrix]

This uses the associativity, commutativity and identity classes recently added to Lean core to define folds with simplification lemmas that can move intermediate results outside the fold for better use in tactics.