At:
paren wf
1
1
1.
T: Type
2.
n: 
3.
s: (T+T) List
4.
s1:(T+T) List. ||s1|| < ||s|| 
paren(T;s1) 
Prop
5.
t: T
6.
s': (T+T) List
7.
s = ([inl(t)] @ s' @ [inr(t)])
||s'|| < ||s||
By:
HypSubst -1 0
THEN
RWW
Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs|| 
0
THEN
Reduce 0
Generated subgoals:
None
About:
