@Begin(Format)@TabSet(1.2inch,1.5 inch)

@b(@ @ @ @ Miscellaneous Rules)
@indexsrule(HYP)@\ @pageref(HYP)@\ Introduce a new hypothesis line into the proof outline.
@indexsrule(LEMMA)@\ @pageref(LEMMA)@\ Introduce a Lemma.
@indexsrule(SAME)@\ @pageref(SAME)@\ Use the fact that two lines are identical to justify a planned line.

@b(@ @ @ @ Propositional Rules)
@indexsrule(CASES)@\ @pageref(CASES)@\ Rule of Cases.
@indexsrule(DEDUCT)@\ @pageref(DEDUCT)@\ The deduction rule.
@indexsrule(DISJ-IMP)@\ @pageref(DISJ-IMP)@\ Rule to replace a disjunction by an implication.
@indexsrule(ECONJ)@\ @pageref(ECONJ)@\ Rule to eliminate a conjunction.
@indexsrule(EQUIV-IMPLICS)@\ @pageref(EQUIV-IMPLICS)@\ Rule to convert an equivalence into twin implications.
@indexsrule(ICONJ)@\ @pageref(ICONJ)@\ Rule to introduce a conjunction.
@indexsrule(IMP-DISJ)@\ @pageref(IMP-DISJ)@\ Rule to replace an implication by a disjunction.
@indexsrule(IMPLICS-EQUIV)@\ @pageref(IMPLICS-EQUIV)@\ Rule to convert twin implications into an equivalence.
@indexsrule(INDIRECT)@\ @pageref(INDIRECT)@\ Rule of Indirect Proof.
@indexsrule(INDIRECT1)@\ @pageref(INDIRECT1)@\ Rule of Indirect Proof using one contradictory line.
@indexsrule(INDIRECT2)@\ @pageref(INDIRECT2)@\ Rule of Indirect Proof using two contradictory lines.
@indexsrule(MP)@\ @pageref(MP)@\ Modus Ponens.

@b(@ @ @ @ Negation Rules)
@indexsrule(ABSURD)@\ @pageref(ABSURD)@\ From falsehood, deduce anything.
@indexsrule(ENEG)@\ @pageref(ENEG)@\ Eliminate a negation.
@indexsrule(INEG)@\ @pageref(INEG)@\ Introduce a negation.
@indexsrule(PULLNEG)@\ @pageref(PULLNEG)@\ Pull out negation.
@indexsrule(PUSHNEG)@\ @pageref(PUSHNEG)@\ Push in negation.

@b(@ @ @ @ Quantifier Rules)
@indexsrule(AB*)@\ @pageref(AB*)@\ Rule to alphabetically change embedded bound variables.
@indexsrule(ABE)@\ @pageref(ABE)@\ Rule to change a top-level occurrence of an existentially
@\ @\ quantified variable.
@indexsrule(ABU)@\ @pageref(ABU)@\ Rule to change a top-level occurrence of a universally quantified
@\ @\ variable.
@indexsrule(EGEN)@\ @pageref(EGEN)@\ Rule of Existential Generalization.
@indexsrule(RULEC)@\ @pageref(RULEC)@\ Rule C.
@indexsrule(UGEN)@\ @pageref(UGEN)@\ Rule of Universal Generalization.
@indexsrule(UI)@\ @pageref(UI)@\ Rule of Universal Instantiation.

@b(@ @ @ @ Substitution Rules)
@indexsrule(SUBSTITUTE)@\ @pageref(SUBSTITUTE)@\ Rule to substitute a term for a variable.

@b(@ @ @ @ Equality Rules)
@indexsrule(EXT=)@\ @pageref(EXT=)@\ Rule of Extensionality.
@indexsrule(EXT=0)@\ @pageref(EXT=0)@\ Rule to derive an equality at type o from an equivalence.
@indexsrule(LET)@\ @pageref(LET)@\ Rule to produce a new variable which will represent an entire
@\ @\ formula during part of a proof.
@indexsrule(SUBST=)@\ @pageref(SUBST=)@\ Substitution of Equality. Performs whichever of the @t(SUBST=L) and @t(SUBST=R) 
@\ @\ rules is appropriate.
@indexsrule(SUBST=L)@\ @pageref(SUBST=L)@\ Substitution of Equality.  Replaces some occurrences of the left hand
@\ @\ side by the right hand side.
@indexsrule(SUBST=R)@\ @pageref(SUBST=R)@\ Substitution of Equality.  Replaces some occurrences of the right
@\ @\ hand side by the left hand side.
@indexsrule(SUBST-EQUIV)@\ @pageref(SUBST-EQUIV)@\ Substitution of Equivalence.
@indexsrule(SYM=)@\ @pageref(SYM=)@\ Symmetry of Equality.

@b(@ @ @ @ Definition Rules)
@indexsrule(EDEF)@\ @pageref(EDEF)@\ Rule to eliminate first definition, left to right.
@indexsrule(EQUIV-WFFS)@\ @pageref(EQUIV-WFFS)@\ Rule to assert equivalence of lines up to definition.
@indexsrule(IDEF)@\ @pageref(IDEF)@\ Rule to introduce a definition.

@b(@ @ @ @ Lambda Conversion Rules)
@indexsrule(LAMBDA*)@\ @pageref(LAMBDA*)@\ Convert between two equivalent lambda-expressions.
@indexsrule(LCONTR*)@\ @pageref(LCONTR*)@\ Rule to put an inferred line into Lambda-normal form.
@indexsrule(LEXPD*)@\ @pageref(LEXPD*)@\ Rule to put a planned line into Lambda-normal form.
@End(Format)


