13. Basic Propositions🔗

With the exception of implication and universal quantification, logical connectives and quantifiers are implemented as inductive types in the Prop universe. In some sense, the connectives described in this chapter are not special—they could be implemented by any user. However, these basic connectives are used pervasively in the standard library and built-in proof automation tools.

1. 13.1. Truth
2. 13.2. Logical Connectives
3. 13.3. Quantifiers
4. 13.4. Propositional Equality