@evgenynr мне Agda сильно больше зашла, эт прям такой трушный Haskell с зависимыми типами. Coq не понравился.