A proof of weak termination of typed λσ-calculi