Entry	Value
Package Name	option-thm
Count	3
Theorems	option_cases : !x. x = NONE \/ (?a. x = SOME a) option_distinct : !a. ~(SOME a = NONE) option_inj : !a b. SOME a = SOME b <=> a = b

Back to main package page