NBE for MiniTT: Why is labelled sum eliminator both a normal form and a neutral value?
They are different things. SClos is a case-split function, which is a function that pattern match on its parameter. Think of it as a lambda (if you know Haskell, you can think of it as a LambdaCase \case, which is a sugared lambda). This is definitely a canonical value in Mini-TT.
The neutral value, OTOH, is an application on a case-split function, where the argument supplied is neutral. If an instance of a sum type is neutral, you don't know which constructor it belongs to, so you don't know which clause in the pattern matching should be selected, so this is a neutral value.
Summary: pattern matching itself is canonical, while application on pattern matching is not. If this application stucks, it becomes a neutral value.