Proving predicate-subtype equivalence

[Alberto Ercolani]

Good day everyone,

I would like to ask for advice for proving an equivalence that is evading me.

In my model sets S and C are complementary, one starts as fullset, the other as emptyset.

Every time I remove an element from S it is inserted in C, the process proceeds until S is not empty.

I'm proving that when S has T elements (all possible elements) then it is fullset.

A single branch is still open, I need to show that:

[-1] forall (q:PROC) : member(q, S) iff not member(q, C)
---
[1] S = {x:PROC|NOT member(x, C)}

Antecedent -1 is a proved lemma modelled by the algorithm, hence valid. PROC = above(1).

How do I show that [1] is true? My difficulty comes from the fact I don't know how to manipulate the dependant type.

Thanks,

Alberto

[Alberto Ercolani]

Extensionality rules did provide me a way to deduce equality. Commands in pages 65 to 68 of the prover manual.