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

At: equal appends eq 1 1 1
1. T: Type
2. x1: T List
3. z: T List
4. x2: T List
5. x3: T List
6. ||x1|| = ||z||
7. (x1 @ x2) = (z @ x3)
8. z = (x1 @ nil)
9. x2 = x3
x1 = z
By: RWO Thm* l:T List. (l @ nil) ~ l -2
Generated subgoals:

None

About:
listnilintuniverseequalsqequalall

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