Lemma 5.3 (Normalisation of values). Every value $1 \to A$ is provably equivalent to a value built from the identity on $1$ using the following constructors: $v \mathbin{;} \mathsf{Left}$ and $v \mathbin{;} \mathsf{Right}$ for values of co-products, $(v, w)$ for values of products, and $v \cdot w$, $[v]$ and $[\,]$ for values of list types.