'ProvenHashes.Halftime.terminal_difference_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'ProvenHashes.Halftime.terminal_length_three_bound' depends on axioms: [propext, Classical.choice, Quot.sound]