{α : Type u} →
  {P : Sort u_1} →
    {toEDist : EDist α} →
      {edist_self : ∀ (x : α), edist x x = 0} →
        {edist_comm : ∀ (x y : α), edist x y = edist y x} →
          {edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z} →
            {toUniformSpace : UniformSpace α} →
              {uniformity_edist :
                  autoParam (uniformity α = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | edist p.1 p.2 < ε})
                    PseudoEMetricSpace.uniformity_edist._autoParam} →
                {toEDist' : EDist α} →
                  {edist_self' : ∀ (x : α), edist x x = 0} →
                    {edist_comm' : ∀ (x y : α), edist x y = edist y x} →
                      {edist_triangle' : ∀ (x y z : α), edist x z ≤ edist x y + edist y z} →
                        {toUniformSpace' : UniformSpace α} →
                          {uniformity_edist' :
                              autoParam (uniformity α = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | edist p.1 p.2 < ε})
                                PseudoEMetricSpace.uniformity_edist._autoParam} →
                            { toEDist := toEDist, edist_self := edist_self, edist_comm := edist_comm,
                                  edist_triangle := edist_triangle, toUniformSpace := toUniformSpace,
                                  uniformity_edist := uniformity_edist } =
                                { toEDist := toEDist', edist_self := edist_self', edist_comm := edist_comm',
                                  edist_triangle := edist_triangle', toUniformSpace := toUniformSpace',
                                  uniformity_edist := uniformity_edist' } →
                              (toEDist ≍ toEDist' → toUniformSpace ≍ toUniformSpace' → P) → P