law works_ok_append

minebender-game@1.0.0.0 · proof_flood.bend:512

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

512law works_ok_append:
513  for +xs: List<&2, G.Work>
514  for +ys: List<&2, G.Work>
515  for +w: Nat
516  for +h: Nat
517  for +layout: T.Grid(Bool)
518  for +p0: T.Pos
519  for +a: {works_ok(xs, w, h, layout, p0) == True{} : Bool}
520  for b: {works_ok(ys, w, h, layout, p0) == True{} : Bool}
521  {works_ok(List.append(&2, G.Work, xs, ys), w, h, layout, p0) == True{} : Bool}