case h.e'_2

⊢ addHaarMeasure Icc01 = ↑↑volume ↑Icc01 • addHaarMeasure Icc01
⊢ addHaarMeasure Icc01 = volume
convert (addHaarMeasure_unique volume Icc01).symm
no goals
case h.e'_2

⊢ addHaarMeasure Icc01 = ↑↑volume ↑Icc01 • addHaarMeasure Icc01
simp [Icc01]