2. n:
3. s: (T+T) List
4.
s1:(T+T) List. ||s1|| < ||s|| 
paren(T;s1) 
Prop5. t: T
6. s': (T+T) List
7. s = ([inl(t)] @ s' @ [inr(t)])
paren(T;s') Type
T:Type, s:(T+T) List. paren(T;s) Prop
| 1 | 1. T: Type 2. n: 3. s: (T+T) List 4. s1:(T+T) List. ||s1|| < ||s|| paren(T;s1) Prop5. t: T 6. s': (T+T) List 7. s = ([inl(t)] @ s' @ [inr(t)]) paren(T;s') Type | 2 steps |
About:
 |  |  |  |  |  |