| ref-0-id-0 | rapport |
| ref-0-id-1 | blank space |
| ref-0-id-2 | mendelson lemma three two a |
| ref-0-id-3 | mendelson lemma three two b |
| ref-0-id-4 | mendelson lemma three two c |
| ref-0-id-5 | mendelson lemma three two d |
| ref-0-id-6 | mendelson lemma three two f |
| ref-0-id-7 | mendelson lemma three two f base |
| ref-0-id-8 | mendelson lemma three two f induction |
| ref-0-id-9 | mendelson lemma three two g |
| ref-0-id-10 | mendelson lemma three two g base |
| ref-0-id-11 | mendelson lemma three two g induction |
| ref-0-id-12 | mendelson lemma three two h |
| ref-0-id-13 | mendelson lemma three two h base |
| ref-0-id-14 | mendelson lemma three two h induction |
| ref-0-id-15 | int mvar |
| ref-0-id-16 | commutative imply |
| ref-0-id-17 | transitive imply |
The pyk compiler, version 0.grue.20050603 by Klaus Grue,