Comment by dependenttypes

It seems somewhat common in cryptography.