The Coq mailing list

[Volker Stolz <stolz+coq AT ifi.uio.no>]

Dear Laurent, dear Amin, thank you for your answers -- unfortunately
they both seem to subvert the spirit of my original problem :-)

So here is my actual problem:

PF is a representation of propositional formulae bool
True/False, props of some type, and negation on disjunction to build
terms. That is, I have terms as a tree structure.

Section PF.
  Variable A : Set.

Inductive pf : Type :=
| bT : pf
| bF : pf
| p (a:A) : pf
| neg (phi:pf) : pf
| or (phi psi: pf) : pf.

Require Import Ensembles.
Require Import Finite_sets.
Require Import Finite_sets_facts.

Fixpoint sf phi : Ensemble pf :=
match phi with
| bT => Singleton pf bT
| bF => Singleton _ bF
| p x => Singleton _ (p x)
| neg phi' => Add _ (sf phi') phi
| or phi' psi' => Add _ (Union _ (sf phi') (sf psi')) phi
end.

And here is my problematic property:

Hypothesis negNotInSelf: forall phi, ~In _ (sf phi) (neg phi).

I.e. sf bT := {bT}, and it does not contain (neg bT). I would hope that
once I've figured that out, the "or" (binary) case would work
analogously. I also tried some variations along the lines of not just
(neg phi), but anything "larger", but didn't have any success with the
formulation.

Best, Volker