def not_and_false

minebender-game@1.0.0.0 · proof_assist.bend:20

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

20def not_and_false(+a: Bool, +b: Bool, e: {Bool.and(Bool.not(a), Bool.not(b)) == False{} : Bool}) ->
21  {Bool.or(a, b) == True{} : Bool}:
22  match a b:
23    case True{} _:
24      {==}
25    case False{} True{}:
26      {==}
27    case False{} False{}:
28      Empty.absurd({False{} == True{} : Bool}, P.true_ne_false(e))