Lemma 3.12 variable typo?

[AlienKevin]

On page 25:

It seems that C should be replaced with D?

Thanks for writing this paper btw, it's really helpful for learning about dependent types. I like how you start from the basics and prove things step by step. Some other papers tend to skip around because they assume more background in the subject.

[hbr]

Typo corrected. Thanks for reporting it.