ProofGen.gen_take: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
Lines 380-397 of minebender-game@1.0.0.0/proof_gen.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_gen.bend&start_line=380&end_line=397

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

def gen_take(+z: G.Zone, +p: T.Pos, +m: Nat, +lp: Nat, +rs: List<&2, U32>,
  inv: {Nat.is_le(1n+m, 1n+lp) == True{} : Bool}, +c: Bool,
  ce: {G.gen.pick(1n+m, 1n+lp, rs) == c : Bool}) ->
  {Nat.add(one(c), Nat.sub(1n+m, one(c))) == 1n+m : Nat} &
  {Nat.is_le(Nat.sub(1n+m, one(c)), Nat.sub(1n+lp, 1n)) == True{} : Bool} &
  {Nat.sub(1n+lp, 1n) == lp : Nat}:
  match c:
    case True{}:
      %Equal.sym(Nat, Nat.sub(m, 0n), m, P.sub_zero(m)) :
        {1n+_ == 1n+m : Nat} & {Nat.is_le(_, Nat.sub(lp, 0n)) == True{} : Bool} &
        {Nat.sub(lp, 0n) == lp : Nat}
      %Equal.sym(Nat, Nat.sub(lp, 0n), lp, P.sub_zero(lp)) :
        {1n+m == 1n+m : Nat} & {Nat.is_le(m, _) == True{} : Bool} & {_ == lp : Nat}
      ({==}, (inv, {==}))
    case False{}:
      %Equal.sym(Nat, Nat.sub(lp, 0n), lp, P.sub_zero(lp)) :
        {1n+m == 1n+m : Nat} & {Nat.is_le(1n+m, _) == True{} : Bool} & {_ == lp : Nat}
      ({==}, (P.le_ne(m, lp, inv, gen_pick_false(1n+m, 1n+lp, rs, ce)), {==}))

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=Zone
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=gen.pick
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=le_ne
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=sub_zero
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=gen_pick_false
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=one
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos