∀ {V : Type u_1} {G : SimpleGraph V} {p₁ p₂ : Set V} (h₁ : G.IsBipartiteWith p₁ p₂) (b : ↑p₁ → ↑p₂)
  (hb₂ : ∀ (a : ↑p₁), G.Adj ↑a ↑(b a)) (v : V) (x : v ∈ (SimpleGraph.hall_subgraph✝ (fun v => ↑(b v)) ⋯ hb₂).verts)
  (h : v ∉ p₁) (x_1 : ↑p₁),
  ((fun a => b a = ⟨v, ⋯⟩) x_1 ∧ ∀ (y : ↑p₁), (fun a => b a = ⟨v, ⋯⟩) y → y = x_1) →
    (∃ (h : ↑x_1 ∈ p₁), ↑(b ⟨↑x_1, ⋯⟩) = v) ∧ ∀ (y : V), (∃ (h : y ∈ p₁), ↑(b ⟨y, ⋯⟩) = v) → y = ↑x_1