| 0 | 0 | propcalc |
| 1 | 0 | nani sete nika...:1 |
| 2 | 0 | axiom one |
| 3 | 0 | axiom two |
| 4 | 0 | axiom three |
| 5 | 0 | nani sete nika...:5 |
| 6 | 0 | nani sete nika...:6 |
| 7 | 0 | rule mp |
| 8 | 0 | nani sete nika...:8 |
| 9 | 0 | mendelson lemma one eight |
| 10 | 0 | nani sete nika...:10 |
| 11 | 0 | nani sete nika...:11 |
| 12 | 0 | nani sete nika...:12 |
| 13 | 0 | nani sete nika...:13 |
| 14 | 0 | lemma id |
| 15 | 2 | * implies * |
The pyk compiler, version 0.grue.20050603 by Klaus Grue,