∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {H : AddSubgroup G}
  {x : AddAction.orbitRel.Quotient G α} {a b : ↑x.orbit} {c : α},
  ⟦a⟧ = ⟦b⟧ → (↑a ∈ AddAction.orbit (↥H) c ↔ ↑b ∈ AddAction.orbit (↥H) c)