'Book18.C₃_comp_K₃' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18.K₃_comp_C₃' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18.orders_differ' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18.same_derivative' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18.C₃_ignores_z' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18.dual_pow' depends on axioms: [propext]
'Book18.C₃_comp_K₃' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18.K₃_comp_C₃' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18.orders_differ' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18.same_derivative' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18.C₃_ignores_z' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18.dual_pow' depends on axioms: [propext]