Mathlib.CategoryTheory.Limits.Unit._auxLemma.1

theorem Mathlib.CategoryTheory.Limits.Unit._auxLemma.1 : ∀ {α : Sort u_1} [inst : Subsingleton α] (x y : α), (x = y) = True

This theorem states that for any type `α` of a certain sort `u_1`, if `α` is a subsingleton (i.e., there is at most one unique element in `α`), then for any two elements `x` and `y` in `α`, `x` is equal to `y`. This is always true because in a subsingleton, all elements are identical.

More concisely: In a subsingleton type `α`, all elements are equal.