Mathlib.CategoryTheory.Sites.Surjective._auxLemma.3

theorem Mathlib.CategoryTheory.Sites.Surjective._auxLemma.3 : ∀ {a : Prop}, (a ↔ True) = a

This theorem, `Mathlib.CategoryTheory.Sites.Surjective._auxLemma.3`, states that for any proposition `a`, the statement that `a` is equivalent to `True` is itself equivalent to `a`. This essentially means that if `a` is true, then it must be equivalent to `True`, and if `a` is equivalent to `True`, then `a` must be true. This theorem is a basic property of logical equivalence in propositional logic.

More concisely: The proposition `a` is logically equivalent to `True` if and only if `a` is true.