At:
paren balance2
2
1
1.
T: Type
2.
s1: (T+T) List
3.
s2: (T+T) List
4.
i:T. (inr(i) 
s1) 
(inl(i) s1)
5.
i:T. (inr(i) s2) (inl(i) s2)
6.
paren(T;s1)
7.
paren(T;s2)
8.
i: T
9.
(inr(i) s1) 
(inr(i) s2)
(inl(i) s1) (inl(i) s2)
By:
Obvious
Generated subgoals:
None
About:
