∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} {a b : G},
  ¬Disjoint (DoubleCoset.doubleCoset a ↑H ↑K) (DoubleCoset.doubleCoset b ↑H ↑K) →
    DoubleCoset.doubleCoset a ↑H ↑K = DoubleCoset.doubleCoset b ↑H ↑K