English
If there exists a unique x with p x and a unique hx for p x with q x hx, then for any y1,y2 with p and q-values, y1 = y2.
Русский
Если есть уникальное x с p(x) и уникальное hx для p(x) с q(x,hx), то любые y1,y2 с p и q образуют равенство y1=y2.
LaTeX
$$$$ (\\\\exists! x, \\exists! hx: p(x), q(x,hx)) \\Rightarrow \\\\forall y_1 y_2, p(y_1) \\land q(y_1, h_{y_1}) \\Rightarrow p(y_2) \\land q(y_2, h_{y_2}) \\Rightarrow y_1 = y_2. $$$$
Lean4
theorem unique₂ {p : α → Sort*} [∀ x, Subsingleton (p x)] {q : ∀ (x : α) (_ : p x), Prop}
(h : ∃! x, ∃! hx : p x, q x hx) {y₁ y₂ : α} (hpy₁ : p y₁) (hqy₁ : q y₁ hpy₁) (hpy₂ : p y₂) (hqy₂ : q y₂ hpy₂) :
y₁ = y₂ := by
simp only [existsUnique_iff_exists] at h
exact h.unique ⟨hpy₁, hqy₁⟩ ⟨hpy₂, hqy₂⟩
