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