doc: mention Props are equal to True or False (#6998)

This PR modifies the `Prop` docstring to point out that every
proposition is propositionally equal to either `True` or `False`. This
will help point users toward seeing that `Prop` is like `Bool`.

I considered mentioning `Classical.propComplete`, but it's probably
better not making it seem like that's how you should work with
propositions.

src/Lean/Parser/Term.lean

@@ -138,7 +138,9 @@ def optSemicolon (p : Parser) : Parser :=
 /-- A specific universe in Lean's infinite hierarchy of universes. -/
 @[builtin_term_parser] def sort := leading_parser
   "Sort" >> optional (checkWsBefore "" >> checkPrec leadPrec >> checkColGt >> levelParser maxPrec)
-/-- The universe of propositions. `Prop ≡ Sort 0`. -/
+/-- The universe of propositions. `Prop ≡ Sort 0`.
+
+Every proposition is propositionally equal to either `True` or `False`. -/
 @[builtin_term_parser] def prop := leading_parser
   "Prop"
 /--