def some_ne_none

minebender-game@1.0.0.0 · proof_solver.bend:906

import Base

906def some_ne_none(-A: Data, -a: A, e: {Some{a} == None{} : Maybe<&2, A>}) -> Empty:
907  %e : disc_some(A, _)
908  Unit{}