title: Can destruct used in implication in Coq?
body: <p><em>destruct</em> can be used to split <em>and</em>, <em>or</em> in Coq. But it seems can also be used in implication?
  For example, I want to prove <code>~~(~~P -&gt; P)</code></p>
  
  <pre><code>Lemma test P : ~~(~~P -&gt; P).
  Proof.
  unfold not.
  intro pffpf.
  apply pffpf.
  intro pff.
  destruct pff.
  intro p.
  apply pffpf.
  intro pff.
  exact p.
  Qed.
  </code></pre>
  
  <p>when <code>destruct pff.</code> it works fine, but I don't know why? Can anyone explain it for me?</p>