def none_ne_some

minebender-game@1.0.0.0 · proof_lists.bend:15

import Base

15def none_ne_some(-A: Data, -x: A, e: {None{} == Some{x} : Maybe<&2, A>}) -> Empty:
16  %e : Maybe.disc_n(A, _)
17  Unit{}