set - Coq 证明补码是对合的

Question

如何证明集合的补集是合合的？

  Require Import Ensembles. Arguments In {_}. Arguments Complement {_}.

  Variables (T:Type) (A:Ensemble T).
  Axiom set_eq: forall (E1 E2:Ensemble T), (forall x, E1 x <-> E2 x) -> E1 = E2.

  Lemma complement_involutive: 
      forall x, In (Complement (Complement A)) x -> In A x.

编辑：假设decidable (In A x)能够firstorder完全证明引理。

Answer 1

complement_involutive正是~ ~ A x -> A x众所周知的等价于排中，在这种情况下 在 中Type，因此如果不将其假设为公理，则无法在 Coq 中证明。请参阅此答案https://math.stackexchange.com/questions/1370805/why-cant-you-prove-the-law-of-the-excluded-middle-in-intuitionistic-logic-for