'LatticeBlockReflection.continuous_retract' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.norm_retract_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.retract_of_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.retract_mul_unit' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.covariant_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.mul_star_of_star_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.covariant_path' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.covariant_average' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.covariant_retract' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.blockmap_equivariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.equivariant_comp' does not depend on any axioms
'LatticeBlockReflection.invariant_pullback' does not depend on any axioms
'LatticeBlockReflection.continuous_path_prod' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.continuous_link' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.continuous_blockmap' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.measurable_refl' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.site_reflection_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.site_reflection_positive_measure' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.pushforward_reflection_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.pullback_mem_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.pushforward_consistent' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.pushforward_reflection_positive_prob' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.pushforward_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
