errors=0 warnings=0
--- axiom footprint summary (unique) ---
  x13  depends on axioms: [propext, Quot.sound]
  x23  depends on axioms: [propext, Classical.choice, Quot.sound]