def PF_both

minebender-game@1.0.0.0 · proof_solver.bend:2740

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

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