Entry | Value |
---|---|
Name | map_option_some |
Conclusion | !f a. map_option f (SOME a) = SOME (f a) |
Constructive Proof | Yes |
Axiom | N|A |
Classical Lemmas | N|A |
Constructive Lemmas | |
Contained Package | option-map-def |
Comment | Standard HOL library retrieved from OpenTheory |