def both_absurd

minebender-game@1.0.0.0 · proof_flood.bend:416

import Base
import minebender-game@1.0.0.0/proof_base.bend as P

416def both_absurd(-A: Type, +a: Bool, e1: {a == False{} : Bool}, e2: {a == True{} : Bool}) -> A:
417  Empty.absurd(A, P.false_ne_true(Equal.trans(Bool, False{}, a, True{}, Equal.sym(Bool, a, False{}, e1), e2)))