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 = lbl .label ↔ lbl = stringvar .label | An Axiom |
| case | ⊦ lbl .label .label = lbl | An Axiom |
| inj | ⊦ stringvar .label = stringvar0 .label ↔ stringvar = stringvar0 | An Axiom |
| sel | ⊦ stringvar .label .label = stringvar | An Axiom |