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

yeah...I am having problems propagating the changes from map simplifications.