matching logic prover support for list segments and overall improvements; more examples

do we need to have some kind of group collection of rules the same way we do with baseTerms? or do you think that the issues that led to that generalization being desirable are not in play here?