law firsts_append

minebender-game@1.0.0.0 · proof_gen.bend:630

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

630law firsts_append:
631  for +z: G.Zone
632  for +xs: List<&2, T.Pos>
633  for +ys: List<&2, T.Pos>
634  {outs(z, List.append(&2, T.Pos, xs, ys)) == Nat.add(outs(z, xs), outs(z, ys)) : Nat}