{Γ : Type u_4} →
  {T : Type u_5} →
    [inst : TopologicalSpace T] →
      [inst_1 : VAdd Γ T] →
        {motive : ProperlyDiscontinuousVAdd Γ T → Sort u} →
          ((finite_disjoint_inter_image :
                ∀ {K L : Set T}, IsCompact K → IsCompact L → {γ | ((fun x => γ +ᵥ x) '' K ∩ L).Nonempty}.Finite) →
              motive ⋯) →
            (t : ProperlyDiscontinuousVAdd Γ T) → motive t