def ev_fb

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/bgcdnat.bend:507

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF

507def ev_fb(+oa: Bool, +ob: Bool, +h: {Bool.not(Bool.or(oa, ob)) == False{} : Bool}, +hoa: {oa == False{} : Bool}) -> {ob == True{} : Bool}:
508  match oa ob:
509    case True{} y:
510      Empty.absurd({y == True{} : Bool}, NF.true_ne_false(hoa))
511    case False{} True{}:
512      {==}
513    case False{} False{}:
514      Empty.absurd({False{} == True{} : Bool}, NF.true_ne_false(h))