@@ -92,6 +92,13 @@ of these patterns.
9292We will return to this function in Section :ref:`sect-provisional` to
9393complete the definition of ``parity``.
9494
95+With and proofs
96+===============
97+To use a dependent pattern match for theorem proving, it is sometimes necessary
98+to explicitly retain and name the proof generated by the pattern match.
99+To do this, you can postfix the with clause with ``proof p`` and the proof
100+generated by the pattern match will be in scope and named ``p``.
101+
95102.. [1] Conor McBride and James McKinna. 2004. The view from the
96103 left. J. Funct. Program. 14, 1 (January 2004),
97104 69-111. DOI=10.1017/S0956796803004829