Conjecture on the interpretation of the substitution rule in ParamDTT

Let $\Gamma$ be a context, let $\b5$ denote one of the modalities of the type theory, and let $t$ be a term. The interpretation of the substitution rule, corresponding to the syntactic admissibility proof, is given by the substitution

$$(\operatorname{id},\mu ! t):\llbracket\Gamma\rrbracket\to\llbracket\Gamma,\mu x:T\rrbracket.$$

Substitution-interpretation conjecture. The interpretation of the substitution rule is given by the substitution above. The source assumes this claim without proof as part of the semantic account of the type theory; the surrounding discussion notes that most of the model remains intact even if it is false.