{P : Sort u} →
  {E : Type u_8} →
    {inst : TopologicalSpace E} →
      {t : ENormedCommMonoid E} →
        {E' : Type u_8} →
          {inst' : TopologicalSpace E'} →
            {t' : ENormedCommMonoid E'} → E = E' → inst ≍ inst' → t ≍ t' → ENormedCommMonoid.noConfusionType P t t'