- allNegAny : All (Not . p) xs -> Not (Any p xs)
If none of the elements satisfy the property, then not any single one can.
Totality: total- anyNegAll : Any (Not . p) xs -> Not (All p xs)
If there exists an element that doesn't satify the property, then it is
not the case that all elements satisfy it.
Totality: total- indexAll : Elem x xs -> All p xs -> p x
Given a proof of membership for some element, extract the property proof for it
Totality: total- negAnyAll : Not (Any p xs) -> All (Not . p) xs
If there does not exist an element that satifies the property, then it is
the case that all elements do not satisfy it.
Totality: total- pullOut : List (Subset a p) -> Subset (List a) (All p)
Pull the elementwise property out to the list level
Totality: total- pushIn : (xs : List a) -> (0 _ : All p xs) -> List (Subset a p)
Push in the property from the list level with element level
Totality: total- pushInOutInverse : (xs : List a) -> (0 prf : All p xs) -> pullOut (pushIn xs prf) = Element xs prf
- Totality: total
- pushOutInInverse : (xs : List (Subset a p)) -> uncurry pushIn (pullOut xs) = xs
- Totality: total