def below_zero_right

stelliferous@0.0.2.0 · proofs/nat_extrema.bend:106

import Base

106def below_zero_right(choice: Bool) -> {False{} == choice && False{} : Bool}:
107  match choice:
108    case False{}: {==}
109    case True{}: {==}