Mathlib.Control.EquivFunctor.Instances._auxLemma.1

theorem Mathlib.Control.EquivFunctor.Instances._auxLemma.1 : ∀ {α : Sort u_1} [inst : Subsingleton α] (x y : α), (x = y) = True

This theorem, named `Mathlib.Control.EquivFunctor.Instances._auxLemma.1`, states that for any sort `α` that has an instance of `Subsingleton` (which means there is at most one element of that type), for any two elements `x` and `y` of `α`, it's always true that `x = y`. In other words, in any type where there can be at most one instance, any two instances of that type must be the same.

More concisely: In a type with at most one element (i.e., a subsingleton type), any two elements are equal.