array
1
Doc
Sections needed for array_1
array
1
int
1
Integer inequalities, subtypes, and induction lemmas for subtypes.
well
fnd
Well-founded predicate. Rank induction lemmas and tactics.
core
Some basic concepts defined type-theoretically.