(*|
冪の古典的性質
==============
|*)

Require Import power.
Require Import classical_logic.
From Stdlib Require Import Logic.FunctionalExtensionality.

Section PowerClassical.
  Context {A : Type}.

  Lemma involutive_complement
    (S : power A)
    : complement (complement S) = S.
  Proof.
    extensionality x.
    unfold complement, mem.
    apply involutive_negation.
  Qed.
End PowerClassical.