law head_some

minebender-game@1.0.0.0 · proof_solver.bend:2497

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

2497law head_some:
2498  for +hs: List<&2, T.Pos>
2499  for +c: T.Pos
2500  for e: {List.head(&2, T.Pos, hs) == Some{c} : Maybe<&2, T.Pos>}
2501  {B.contains(hs, c) == True{} : Bool}