continued working on xFoldl postcondition