law at_set_eq
minebender-game@1.0.0.0 · proof_lists.bend:205
import minebender-game@1.0.0.0/proof_lists.bend as ProofLists
import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/board.bend as B
205law at_set_eq:
206 for -A: Data
207 for +w: Nat
208 for +h: Nat
209 for +g: T.Grid(A)
210 for +x: Nat
211 for +y: Nat
212 for +v: A
213 for +d: A
214 for +sh: {B.shaped(A, w, h, g) == True{} : Bool}
215 for +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}
216 {B.at(A, d, B.set_at(A, g, T.Pos{x, y}, v), T.Pos{x, y}) == v : A}