Entry	Value
Package Name	list-nub-thm
Count	8
Theorems	length_nub : !l. LENGTH (nub l) <= LENGTH l length_setify : !l. LENGTH (setify l) <= LENGTH l mem_nub : !l x. MEM x (nub l) <=> MEM x l mem_setify : !l x. MEM x (setify l) <=> MEM x l nub_idempotent : !l. nub (nub l) = nub l set_of_list_nub : !l. set_of_list (nub l) = set_of_list l set_of_list_setify : !l. set_of_list (setify l) = set_of_list l setify_idempotent : !l. setify (setify l) = setify l

Back to main package page