At:
paren order1
3
2
1
1
3
1
1
1.
T: Type
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)
13.
e1: (T+T) List
14.
s = (e @ e1)
15.
([inl(i)] @ s2) = (e1 @ [inr(t)])
16.
e2: (T+T) List
17.
[inl(i)] = (e1 @ e2)
18.
[inr(t)] = (e2 @ s2)
19.
e2 = nil
20.
e1 = [inl(i)]
21.
e2 = nil
22.
s2 = [inr(t)]
e1 = ([inl(i)] @ nil) (T+T) List
By:
ObviousFrom [-3]
Generated subgoals:
None
About:
