This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| characteristic-function | ⊦ χ(s)(a) ↔ a ∈ s | An Axiom |
| construct-set | ⊦ a ∈ {f} ↔ f(a) | An Axiom |