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