def gen_some_ne_none

minebender-game@1.0.0.0 · proof_gen.bend:140

import Base

140def gen_some_ne_none(-A: Data, -a: A, e: {Some{a} == None{} : Maybe<&2, A>}) -> Empty:
141  %e : Maybe.disc_some(A, _)
142  Unit{}