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

import Base

law Bq.and_intro:
  (@+x_0: Bool -> (@+y_1: Bool -> (@+ex_2: {x_0 == True{} : Bool} -> (@+ey_3: {y_1 == True{} : Bool} -> {Bq.Bool.and(x_0, y_1) == True{} : Bool}))))

Uses (3):
  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.Bool.and