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

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

About: