Indeed, there are other invariants to type systems that are much better than cut...

		noosphr 18 hours ago \| parent \| context \| favorite \| on: Typechecking is undecidable when 'type' is a type ... Indeed, there are other invariants to type systems that are much better than cutting off your toes.