At:
paren induction
3
1.
T: Type
2.
P: ((T+T) List)
Prop
3.
P(nil)
4.
s1,s2:(T+T) List. P(s1) 
P(s2) paren(T;s1) paren(T;s2) P(s1 @ s2)
5.
s:(T+T) List, t:T. P(s) paren(T;s) P([inl(t)] @ s @ [inr(t)])
6.
n: 
7.
s: (T+T) List
8.
s1:(T+T) List. ||s1|| < ||s|| paren(T;s1) P(s1)
9.
s': (T+T) List
10.
s'': (T+T) List
11.
||s'|| < ||s||
12.
||s''|| < ||s||
13.
s = (s' @ s'')
14.
paren(T;s')
15.
paren(T;s'')
P(s)
By:
HypSubst -3 0
THEN
BackThru 4
THEN
BackThruSomeHyp
Generated subgoals:
None
About:
