s:(T+T) List, t:T. (i:T, s1,s2:(T+T) List. s = (s1 @ [inl(i)] @ s2) (inr(i) s2)) paren(T;s) (i:T, s1,s2:(T+T) List. ([inl(t)] @ s @ [inr(t)]) = (s1 @ [inl(i)] @ s2) (inr(i) s2))

1	2. s: (T+T) List 3. t: T 4. i:T, s1,s2:(T+T) List. s = (s1 @ [inl(i)] @ s2) (inr(i) s2) 5. paren(T;s) 6. i: T 7. s1: (T+T) List 8. s2: (T+T) List 9. ([inl(t)] @ s @ [inr(t)]) = (s1 @ [inl(i)] @ s2) 10. e: (T+T) List 11. [inl(t)] = (s1 @ e) 12. ([inl(i)] @ s2) = (e @ s @ [inr(t)]) (inr(i) s2)	12 steps
2	2. s: (T+T) List 3. t: T 4. i:T, s1,s2:(T+T) List. s = (s1 @ [inl(i)] @ s2) (inr(i) s2) 5. paren(T;s) 6. i: T 7. s1: (T+T) List 8. s2: (T+T) List 9. ([inl(t)] @ s @ [inr(t)]) = (s1 @ [inl(i)] @ s2) 10. e: (T+T) List 11. s1 = ([inl(t)] @ e) 12. (s @ [inr(t)]) = (e @ [inl(i)] @ s2) (inr(i) s2)	18 steps

About: