Subset
Exists
The ports are rather straight forward and I have purposefully written the documentation to be beginner friendly. Note, I have diverged from Idris1 over the naming of the projection functions to make them consistent with `Pair` and `DPair`.