BooleanLogic.every_condition_holds: law of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/boolean_logic.bend as BooleanLogic
Lines 60-64 of stelliferous@0.0.2.0/proofs/boolean_logic.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/boolean_logic.bend&start_line=60&end_line=64

import Base

law every_condition_holds:
  for +conditions: List<&2,Bool>
  for +index: Nat
  for truth: {all(conditions) == True{} : Bool}
  {condition_at(conditions,index) == True{} : Bool}

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=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/boolean_logic.bend&name=all
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/boolean_logic.bend&name=condition_at
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/boolean_logic.bend&name=left
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/boolean_logic.bend&name=right