def wcontains_append_l.go

minebender-game@1.0.0.0 · proof_flood.bend:180

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

180def wcontains_append_l.go(+c: T.Pos, +t: List<&2, G.Work>, +ys: List<&2, G.Work>, +q: T.Pos, +b: Bool,
181  e: {Bool.or(b, wcontains(t, q)) == True{} : Bool},
182  ih: {wcontains(t, q) == True{} : Bool} -> {wcontains(List.append(&2, G.Work, t, ys), q) == True{} : Bool}) ->
183  {Bool.or(b, wcontains(List.append(&2, G.Work, t, ys), q)) == True{} : Bool}:
184  match b:
185    case True{}:
186      {==}
187    case False{}:
188      ih(e)