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