P:(((T+T) List)
Prop). P(nil) 
(s1,s2:(T+T) List. P(s1) P(s2) paren(T;s1) paren(T;s2) P(s1 @ s2)) (s:(T+T) List, t:T. P(s) paren(T;s) P([inl(t)] @ s @ [inr(t)])) (s:(T+T) List. paren(T;s) P(s))as,bs:T List. ||as @ bs|| = ||as||+||bs|| 
