- Use propositions in more complex ways
- Build logical connectives to build propositions.
- User tactics to construct proofs with more complex propositions.
- Understand the source of some of Coq’s restrictions.
All the material for this topic is contained in the Logic in Coq chapter of Software Foundations.