(3steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: member reverse 2
1. T: Type
2. x: T
3. L: T List
4. u: T
5. v: T List
6. (x rev(v)) (x v)
7. (x rev(v)) (x v)
8. x = u (x v)
(x rev(v)) x = u (x nil)
By: Obvious
Generated subgoals:

None

About:
listniluniverseequalimpliesor

(3steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc