{P : Sort u} →
  {τ : Type u_1} →
    {inst : TopologicalSpace τ} →
      {inst_1 : AddMonoid τ} →
        {inst_2 : ContinuousAdd τ} →
          {α : Type u_2} →
            {inst_3 : TopologicalSpace α} →
              {t : Flow τ α} →
                {τ' : Type u_1} →
                  {inst' : TopologicalSpace τ'} →
                    {inst'_1 : AddMonoid τ'} →
                      {inst'_2 : ContinuousAdd τ'} →
                        {α' : Type u_2} →
                          {inst'_3 : TopologicalSpace α'} →
                            {t' : Flow τ' α'} →
                              τ = τ' →
                                inst ≍ inst' →
                                  inst_1 ≍ inst'_1 →
                                    inst_2 ≍ inst'_2 → α = α' → inst_3 ≍ inst'_3 → t ≍ t' → Flow.noConfusionType P t t'