'ActualMathematics.RetentionSpatial.roundtrip' depends on axioms: [propext, Classical.choice, Quot.sound] 'ActualMathematics.RetentionSpatial.deformation_preserves_tallies' depends on axioms: [propext, Classical.choice, Quot.sound] 'ActualMathematics.RetentionSpatial.joining_paths' depends on axioms: [propext, Classical.choice, Quot.sound] 'ActualMathematics.RetentionSpatial.joined_paths_count' depends on axioms: [propext, Classical.choice, Quot.sound] 'ActualMathematics.RetentionSpatial.joined_paths_net' depends on axioms: [propext, Classical.choice, Quot.sound] 'ActualMathematics.RetentionSpatial.backtrack_is_retained' depends on axioms: [propext, Classical.choice, Quot.sound] 'ActualMathematics.RetentionSpatial.two_acts_differ_from_empty' depends on axioms: [propext, Classical.choice, Quot.sound]