冪の古典的性質

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.A: Type
S: power A
complement (complement S) = S
  Proof.A: Type
S: power A
complement (complement S) = S
    extensionality x.A: Type
S: power A
x: A
complement (complement S) x = S x
    unfold complement, mem.A: Type
S: power A
x: A
(~ ~ S x) = S x
    apply involutive_negation.
  Qed.
End PowerClassical.