ProofDisplay.over_cell: law of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_display.bend as ProofDisplay
Lines 195-205 of minebender-game@1.0.0.0/proof_display.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_display.bend&start_line=195&end_line=205

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/LAWS.bend as L

# A mine, once the game is over, under each way the cell might be marked.
law over_cell:
  for +c: Bool
  for +st: T.Status
  for over: {st != T.Playing{} : T.Status}
  for +fl: Bool
  for +w: Nat
  for +h: Nat
  for +layout: T.Grid(Bool)
  for +p: T.Pos
  {L.is_covered(G.tile.go(None{}, c, True{}, fl, st, w, h, layout, p)) == False{} : Bool}

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=is_covered
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=tile.go
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=tile_hidden
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Grid
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Status