English
The elimination arrow injArrow encodes that from equality (x1,y1)=(x2,y2) we can derive any property P given x1 = x2 and y1 = y2; it embodies the no-confusion principle for pairs.
Русский
Стрела исключения injArrow кодирует бессмысленность смешения: из равенства (x1,y1)=(x2,y2) следует, что при равенствах x1=x2 и y1=y2 выполняется любое свойство P.
LaTeX
$$$$ \\text{injArrow}\\; h\\; P = P \\quad\\text{(при } h:\\,(x_1,y_1)=(x_2,y_2)\\text{)} $$$$
Lean4
def injArrow {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} : (x₁, y₁) = (x₂, y₂) → ∀ ⦃P : Sort*⦄, (x₁ = x₂ → y₁ = y₂ → P) → P :=
fun h₁ _ h₂ ↦ Prod.noConfusion h₁ h₂
