ProofGen.opening_in: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
Lines 321-325 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=321&end_line=325

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/board.bend as B
import minebender-game@1.0.0.0/game.bend as G
import minebender-game@1.0.0.0/LAWS.bend as L

# A wide zone holds every cell next to the first click.
def opening_in(+first: T.Pos, +p: T.Pos, +wide: Bool, ew: {wide == True{} : Bool},
  near: {L.within_one(first, p) == True{} : Bool}) -> {G.gen.out(G.Zone{first, wide}, p) == True{} : Bool}:
  %Equal.sym(Bool, wide, True{}, ew) : {G.gen.out(G.Zone{first, _}, p) == True{} : Bool}
  Equal.trans(Bool, B.within_one(first, p), L.within_one(first, p), True{}, within_eq(first, p), near)

Uses (9):
  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=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=within_one
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=within_one
  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.out
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=within_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos