'CoarseFaceHodgeSplit.range_sup_tags' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseFaceHodgeSplit.disjoint_range_tags' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseFaceHodgeSplit.finrank_ker_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseFaceHodgeSplit.decomp_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseFaceHodgeSplit.norm_sq_add_harmonic' depends on axioms: [propext, Classical.choice, Quot.sound]
