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: |
|---|---|---|
| gen | An Axiom | |
| elim | ⊦ stringvar = class .class ↔ class = stringvar .class | An Axiom |
| case | ⊦ class .class .class = class | An Axiom |
| inj | ⊦ stringvar .class = stringvar0 .class ↔ stringvar = stringvar0 | An Axiom |
| sel | ⊦ stringvar .class .class = stringvar | An Axiom |