Game.Bq.rejected_op_is_noop: law of gralha-bendquest@0.1.0.0
Import: import gralha-bendquest@0.1.0.0/game.bend as Game
Lines 646-647 of gralha-bendquest@0.1.0.0/game.bend: https://jend.leeeet.dev/read.txt?path=gralha-bendquest@0.1.0.0/game.bend&start_line=646&end_line=647

import Base

law Bq.rejected_op_is_noop:
  (@+op_0: Bq.HOp -> (@+h_1: Bq.Hero -> (@+__2: {Bq.hop_ok(op_0, h_1) == False{} : Bool} -> {Bq.hero_step(op_0, h_1) == h_1 : Bq.Hero})))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.HOp
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Hero
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.hero_step
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.hero_step_go
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.hop_ok