More generally, ticks can be used to encode [1]} the delayed substitutions of [2]},
which have been used to reason coinductively about coinductive data. For more examples of
reasoning using these see [2]}.
The tick calculus is an example of a Fitch-style modal
calculus [4]}, [5]}. Most of these use a presentation
where ticks are simply markers in the context, rather than carry names as here. However,
names of ticks play a crucial role in the normalisation proof for CloTT [1]},
and we therefore also use names here.
