На самом деле для того, чтобы поиграться с зависимыми типами и получить базовое представление о них советую посмотреть на интерактивный онлайн туториал по F*, он достаточно понятный и при этом основные идеи донесет:
https://www.fstar-lang.org/tutorial/
Плюсую.