∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [T2Space X] [DiscreteTopology G] [ContinuousConstSMul G X]
  [CompactlyGeneratedSpace (X × X)], ProperlyDiscontinuousSMul G X ↔ ProperSMul G X