{P : Sort u} →
  {E : Type u_3} →
    {inst : NormedAddCommGroup E} →
      {inst_1 : NormedSpace ℝ E} →
        {t : ContDiffBumpBase E} →
          {E' : Type u_3} →
            {inst' : NormedAddCommGroup E'} →
              {inst'_1 : NormedSpace ℝ E'} →
                {t' : ContDiffBumpBase E'} →
                  E = E' → inst ≍ inst' → inst_1 ≍ inst'_1 → t ≍ t' → ContDiffBumpBase.noConfusionType P t t'