'Kenoma.Arm.upward_mass_event_work_numerator' depends on axioms: [propext, Quot.sound]
'Kenoma.Arm.shared_guide_force_balance' depends on axioms: [propext, Quot.sound]
'Kenoma.Arm.contact_partition_area_numerator' depends on axioms: [propext]
'Kenoma.Arm.conservative_contact_gap' depends on axioms: [propext, Classical.choice, Quot.sound]