Game.Bq.quaff_burns_one_potion: law of gralha-bendquest@0.1.0.0
Import: import gralha-bendquest@0.1.0.0/game.bend as Game
Lines 970-971 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=970&end_line=971

import Base

law Bq.quaff_burns_one_potion:
  (@+h_0: Bq.Hero -> (@+__1: {Bq.quaff_ok(h_0) == True{} : Bool} -> {Bq.Bag.add(Bq.one(Bq.POTION), Bq.census(Bq.hero_step(Bq.HOp.Quaff{}, h_0))) == Bq.census(h_0) : Bq.Bag}))

Uses (24):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bag
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bag.add
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bag.add_assoc
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bag.add_sub_cancel
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bag.le
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bag.sub
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bool.false_ne_true
  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.Maybe
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.POTION
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.census
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.gear_bag
  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.mb
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.one
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.quaff_ok