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

import Base

law Bq.equip_shuffle:
  (@+i_0: Bq.Bag -> (@+k1_1: Bq.Bag -> (@+r_2: Bq.Bag -> (@+has_3: {Bq.Bag.le(k1_1, i_0) == True{} : Bool} -> {Bq.Bag.add(Bq.Bag.sub(i_0, k1_1), Bq.Bag.add(k1_1, r_2)) == Bq.Bag.add(i_0, r_2) : Bq.Bag}))))

Uses (11):
  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=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.bag_swap