{P : Sort u} →
  {E : Type u_2} →
    {F : Type u_3} →
      {inst : NormedAddCommGroup E} →
        {inst_1 : NormedSpace ℝ E} →
          {inst_2 : NormedAddCommGroup F} →
            {inst_3 : NormedSpace ℝ F} →
              {n : ℕ∞} →
                {K : TopologicalSpace.Compacts E} →
                  {t : ContDiffMapSupportedIn E F n K} →
                    {E' : Type u_2} →
                      {F' : Type u_3} →
                        {inst' : NormedAddCommGroup E'} →
                          {inst'_1 : NormedSpace ℝ E'} →
                            {inst'_2 : NormedAddCommGroup F'} →
                              {inst'_3 : NormedSpace ℝ F'} →
                                {n' : ℕ∞} →
                                  {K' : TopologicalSpace.Compacts E'} →
                                    {t' : ContDiffMapSupportedIn E' F' n' K'} →
                                      E = E' →
                                        F = F' →
                                          inst ≍ inst' →
                                            inst_1 ≍ inst'_1 →
                                              inst_2 ≍ inst'_2 →
                                                inst_3 ≍ inst'_3 →
                                                  n = n' →
                                                    K ≍ K' → t ≍ t' → ContDiffMapSupportedIn.noConfusionType P t t'