Nuprl - Proof: paren balance2 2

(5steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

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 @ s2)

(inl(i) s1 @ s2)

By: All (RWO Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2))

Generated subgoal:

1 9. (inr(i) s1) (inr(i) s2)
(inl(i) s1) (inl(i) s2) 1 step

About:

(5steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc