2. L: T List
3. x: T
4. y: T
5. x before y
L
A,B:T List. L = (A @ B) & (x A) & (y B)2. L: T List
3. x: T
4. y: T
5.
A,B:T List. L = (A @ B) & (x A) & (y B) x before y L
T:Type, L:T List, x,y:T. x before y L 
(A,B:T List. L = (A @ B) & (x A) & (y B))
| 1 | 1. T: Type 2. L: T List 3. x: T 4. y: T 5. x before y L A,B:T List. L = (A @ B) & (x A) & (y B) | 9 steps |
| 2 | 1. T: Type 2. L: T List 3. x: T 4. y: T 5. A,B:T List. L = (A @ B) & (x A) & (y B) x before y L | 1 step |
About:
 |  |  |  |  |  |