причём там была (умышленная) ошибка, off-by-one — но тайпчекер даже после исправления грит, мол не может унифицировать `Nat` и `Fin n`, очень удобно