[Proof of Lemma REF ]
As in [1]} this is proved by induction on the sizes of the terms, contexts, and
types involved, simultaneously with Theorem REF  and the three lemmas above.
Most cases are standard, including the cases for universal quantification over clocks which is modelled
here as a \(\Pi \) -type. We just explain the non-standard cases.
