law inv_play

minebender-game@1.0.0.0 · proof_inv.bend:795

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

795law inv_play:
796  for +w: Nat
797  for +h: Nat
798  for +layout: T.Grid(Bool)
799  for +acts: List<&2, T.Action>
800  for +g: G.Game
801  for inv: Inv(w, h, layout, g)
802  Inv(w, h, layout, L.play(acts, g))