def pick_le1

minebender-game@1.0.0.0 · proof_gen.bend:1001

import Base

1001def pick_le1(+b: Bool) -> {Nat.is_le(Bool.pick(Nat, b, 1n, 0n), 1n) == True{} : Bool}:
1002  match b:
1003    case True{}:
1004      {==}
1005    case False{}:
1006      {==}