At:
paren order1
2
1
1
2
1
1
1.
T: Type
2.
s1: (T+T) List
3.
s2: (T+T) List
4.
i:T, s1@0,s2:(T+T) List. s1 = (s1@0 @ [inl(i) / s2]) 
(inr(i) 
s2)
5.
i:T, s1,s2@0:(T+T) List. s2 = (s1 @ [inl(i) / s2@0]) (inr(i) s2@0)
6.
paren(T;s1)
7.
paren(T;s2)
8.
i: T
9.
s1@0: (T+T) List
10.
s2@0: (T+T) List
11.
(s1 @ s2) = (s1@0 @ [inl(i) / s2@0])
12.
u: T+T
13.
v: (T+T) List
14.
s1 = (s1@0 @ [u / v])
15.
[inl(i) / s2@0] = [u / (v @ s2)]
16.
e1: (T+T) List
17.
s2 = (e1 @ s2@0)
18.
inl(i) = u
19.
nil = (v @ e1)
s1 = (s1@0 @ [inl(i) / v])
By:
SubstFor u -6
THEN
Reduce -6
Generated subgoals:
None
About:
