{P : Sort u} →
  {E : Type uE} →
    {inst : NormedAddCommGroup E} →
      {inst_1 : NormedSpace ℝ E} →
        {H : Type uH} →
          {inst_2 : TopologicalSpace H} →
            {I : ModelWithCorners ℝ E H} →
              {M : Type uM} →
                {inst_3 : TopologicalSpace M} →
                  {inst_4 : ChartedSpace H M} →
                    {c : M} →
                      {t : SmoothBumpFunction I c} →
                        {E' : Type uE} →
                          {inst' : NormedAddCommGroup E'} →
                            {inst'_1 : NormedSpace ℝ E'} →
                              {H' : Type uH} →
                                {inst'_2 : TopologicalSpace H'} →
                                  {I' : ModelWithCorners ℝ E' H'} →
                                    {M' : Type uM} →
                                      {inst'_3 : TopologicalSpace M'} →
                                        {inst'_4 : ChartedSpace H' M'} →
                                          {c' : M'} →
                                            {t' : SmoothBumpFunction I' c'} →
                                              E = E' →
                                                inst ≍ inst' →
                                                  inst_1 ≍ inst'_1 →
                                                    H = H' →
                                                      inst_2 ≍ inst'_2 →
                                                        I ≍ I' →
                                                          M = M' →
                                                            inst_3 ≍ inst'_3 →
                                                              inst_4 ≍ inst'_4 →
                                                                c ≍ c' →
                                                                  t ≍ t' → SmoothBumpFunction.noConfusionType P t t'