{P : Sort u_1} →
  {α : Type u} →
    {β : Type v} →
      {inst : PseudoEMetricSpace α} →
        {inst_1 : PseudoEMetricSpace β} →
          {t : α ≃ᵢ β} →
            {α' : Type u} →
              {β' : Type v} →
                {inst' : PseudoEMetricSpace α'} →
                  {inst'_1 : PseudoEMetricSpace β'} →
                    {t' : α' ≃ᵢ β'} →
                      α = α' → β = β' → inst ≍ inst' → inst_1 ≍ inst'_1 → t ≍ t' → IsometryEquiv.noConfusionType P t t'