minor cleanup in proof of sequential composition