Moved some level list proofs into SfLib
proof for cut_list_left_app.