Macros§
- assert_
sets_ equal - Prove two sets equal by extensionality. Usage is:
Functions§
- axiom_
is_ empty - axiom_
is_ empty_ len0 - group_
set_ lib_ default - group_
set_ properties - lemma_
int_ range - lemma_
len_ difference - lemma_
len_ intersect - lemma_
len_ subset - lemma_
len_ union - lemma_
len_ union_ ind - lemma_
map_ size - lemma_
set_ difference2 - lemma_
set_ difference_ len - lemma_
set_ disjoint - lemma_
set_ disjoint_ lens - lemma_
set_ empty_ equivalency_ len - lemma_
set_ insert_ finite_ iff - lemma_
set_ intersect_ again1 - lemma_
set_ intersect_ again2 - lemma_
set_ intersect_ union_ lens - lemma_
set_ properties Deprecated - lemma_
set_ remove_ finite_ iff - lemma_
set_ subset_ finite - lemma_
set_ union_ again1 - lemma_
set_ union_ again2 - lemma_
set_ union_ finite_ iff - lemma_
set_ union_ finite_ implies_ sets_ finite - lemma_
sets_ eq_ iff_ injective_ map_ eq - lemma_
subset_ equality - set_
int_ range