law row_false_set

minebender-game@1.0.0.0 · proof_lists.bend:466

import Base
import minebender-game@1.0.0.0/board.bend as B

466law row_false_set:
467  for +r: List<&2, Bool>
468  for +x: Nat
469  for e: {List.get(&2, Bool, r, x) == Some{False{}} : Maybe<&2, Bool>}
470  {B.row_false(r) == 1n+B.row_false(List.set(&2, Bool, r, x, True{})) : Nat}