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

At: equal appends eq 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 = (nil @ x3)
x1 = z & x2 = x3
By: All Reduce
Generated subgoal:

19. x2 = x3
x1 = z		1 step

About:
listnilintuniverseequaland

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