Part I: Dependent Types

This part is an introduction to the actual practices of working with dependent types in Arend. It contains example-based Arend-specific exposition of efficient ways of working with propositions and proofs, inductive types, classes and records, type universes, etc. We assume that the reader is familiar with basic concepts from ML-like languages (such as Haskell, Agda, or Coq/Gallina).