| choice 1 | |
| rel 1 | Common properties of binary relations. |
| bool 1 | Definitions, theorems and tactics for the boolean type and boolean-related expressions. |
| int 1 | Integer inequalities, subtypes, and induction lemmas for subtypes. |
| well fnd | Well-founded predicate. Rank induction lemmas and tactics. |
| fun 1 | Polymorphic identity and composition functions. Lemmas covering properties such as injectivity and surjectivity. |
| core | Some basic concepts defined type-theoretically. |