'IncidenceCubes.Penrose.bottom_edge' depends on axioms: [propext, Quot.sound]
'IncidenceCubes.Penrose.middle_edge' depends on axioms: [propext, Quot.sound]
'IncidenceCubes.Penrose.top_edge' depends on axioms: [propext, Quot.sound]
'IncidenceCubes.Penrose.exists_algebraic_eighth' depends on axioms: [propext, Quot.sound]
'IncidenceCubes.Penrose.face_pencil_identity' depends on axioms: [propext, Quot.sound]
'IncidenceCubes.Penrose.top_face_common_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'IncidenceCubes.Penrose.polar_rank_one_update' depends on axioms: [propext, Quot.sound]
'IncidenceCubes.Penrose.polar_agrees_on_chord' depends on axioms: [propext, Quot.sound]
'IncidenceCubes.Fomin.total_product' depends on axioms: [propext, Classical.choice, Quot.sound]
'IncidenceCubes.Fomin.last_face' depends on axioms: [propext, Classical.choice, Quot.sound]
'IncidenceCubes.Fomin.cube_last_face' depends on axioms: [propext, Classical.choice, Quot.sound]
'IncidenceCubes.Fomin.cross_dot_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'IncidenceCubes.Fomin.ratio_one_iff_incident' depends on axioms: [propext, Classical.choice, Quot.sound]
'IncidenceCubes.Connection.eval_doubleLine' depends on axioms: [propext, Classical.choice, Quot.sound]
'IncidenceCubes.Connection.doubleLine_rescale' depends on axioms: [propext, Classical.choice, Quot.sound]
'IncidenceCubes.Connection.doubleLine_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'IncidenceCubes.Connection.rank_one_pencil' depends on axioms: [propext, Classical.choice, Quot.sound]