2. u: T+T
3. v: (T+T) List
4. u1: T+T
5. v1: (T+T) List
6. paren(T;[u / v])
7. paren(T;[u1 / v1])
paren(T;[u1 / v1] @ [u / v])
T:Type, s',s3:(T+T) List. paren(T;s') 
paren(T;s3) paren(T;s3 @ s')
as:T List. (as @ nil) = as
0)
| 1 | 1. T: Type 2. u: T+T 3. v: (T+T) List 4. u1: T+T 5. v1: (T+T) List 6. paren(T;[u / v]) 7. paren(T;[u1 / v1]) paren(T;[u1 / v1] @ [u / v]) | 1 step |
About:
 |  |  |  |  |  |  |  |