<span><strong class="command">P</strong></span>.</p><p>If <span><strong class="command">p</strong></span> is provided, it must be a proof term for
<span><strong class="command">P</strong></span>. Otherwise an interactive proof is started.</p><p><span><strong class="command">P</strong></span> can be omitted only if the proof is not
interactive.</p><p>Proving a theorem already proved in the library is an error.
<span><strong class="command">P</strong></span>.</p><p>If <span><strong class="command">p</strong></span> is provided, it must be a proof term for
<span><strong class="command">P</strong></span>. Otherwise an interactive proof is started.</p><p><span><strong class="command">P</strong></span> can be omitted only if the proof is not
interactive.</p><p>Proving a theorem already proved in the library is an error.