- From non-dependent signature
`S`

to dependent signature`Sdep`

. - From dependent signature
`Sdep`

to non-dependent signature`S`

.

- Red-black trees
- Occurrence in a tree
- Binary search trees
- Balanced red-black trees
- Sets as red-black trees
- Logical appartness
- Empty set
- Emptyness test
- Appartness
- Singleton set
- Insertion
- Deletion
- From lists to red-black trees
- Elements
- Isomorphism with
`FSetList`

- Union
- Intersection
- Difference
- Equality test
- Inclusion test
- Fold
- Cardinal
- Filter
- Minimum element
- Maximum element
- Any element
- Comparison

- Trees
- Occurrence in a tree
- Binary search trees
- AVL trees
- Sets as AVL trees
- Logical appartness
- Empty set
- Emptyness test
- Appartness
- Singleton set
- Helper functions
- Insertion
- Join
- Extraction of minimum and maximum element
- Merging two trees
- Deletion
- Minimum element
- Maximum element
- Any element
- Concatenation
- Splitting
- Intersection
- Difference
- Elements
- Cardinal
- Union
- Filter
- Partition
- Subset
- Fold
- Comparison
- Equality test

This page has been generated by coqdoc