'CoarseFaceFourTorusTags.bianchi' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseFaceFourTorusTags.flux_mem_tags' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseFaceFourTorusTags.flux_linearIndependent' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseFaceFourTorusTags.six_le_finrank_tags' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseFaceFourTorusTags.disjoint_range_tags' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseFaceFourTorusTags.finrank_ker_d2_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
