'Book24LM.theorem1a' depends on axioms: [propext, Quot.sound]
'Book24LM.theorem1b' depends on axioms: [propext, Quot.sound]
'Book24LM.theorem2' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24LM.corollaryA' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24LM.corollaryB' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24LM.control_corollaryB_needs_trivial_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24LM.interpolation' depends on axioms: [propext, Classical.choice, Quot.sound]