T:Type, s':(T+T) List. paren(T;s') (i:T. (inr(i) s') (inl(i) s'))

1	1. T: Type 2. i: T 3. (inr(i) nil) (inl(i) nil)	1 step
2	1. T: Type 2. s1: (T+T) List 3. s2: (T+T) List 4. i:T. (inr(i) s1) (inl(i) s1) 5. i:T. (inr(i) s2) (inl(i) s2) 6. paren(T;s1) 7. paren(T;s2) 8. i: T 9. (inr(i) s1 @ s2) (inl(i) s1 @ s2)	2 steps
3	1. T: Type 2. s': (T+T) List 3. t: T 4. i:T. (inr(i) s') (inl(i) s') 5. paren(T;s') 6. i: T 7. (inr(i) [inl(t)] @ s' @ [inr(t)]) (inl(i) [inl(t)] @ s' @ [inr(t)])	1 step

About: