{P : Sort u} →
  {α : Type u_1} →
    {m0 : MeasurableSpace α} →
      {μ : MeasureTheory.Measure α} →
        {C : Set (Set α)} →
          {t : μ.FiniteSpanningSetsIn C} →
            {α' : Type u_1} →
              {m0' : MeasurableSpace α'} →
                {μ' : MeasureTheory.Measure α'} →
                  {C' : Set (Set α')} →
                    {t' : μ'.FiniteSpanningSetsIn C'} →
                      α = α' →
                        m0 ≍ m0' →
                          μ ≍ μ' → C ≍ C' → t ≍ t' → MeasureTheory.Measure.FiniteSpanningSetsIn.noConfusionType P t t'