A brief explanation of base cases
According to the sentence, the conjecture being proved is
``reversing the reverse of a
(implies (true-listp z) (equal (rev (rev z)) z)).
We're also told that this is an inductive proof. Evidently we're doing an
induction on the structure of the list
(implies (endp z) (implies (true-listp z) (equal (rev (rev z)) z))).
Now use your browser's Back Button to return to the example proof in logic-knowledge-taken-for-granted.