Corollary.  [pagin2021-mdl]

Given a complex indirect constant μ-system, for any term t, there is some minimum derivation length to a unique normal form.