Nuprl - graph_1_2 LEMMAs for paren

Rank	Theorem	Name
3	Thm* s':(T+T) List. paren(T;s') (i:T. (inl(i) s') (inr(i) s'))	[paren_balance1]
cites
1	Thm* P:(((T+T) List)Prop). P(nil) (s1,s2:(T+T) List. P(s1) P(s2) paren(T;s1) paren(T;s2) P(s1 @ s2)) (s:(T+T) List, t:T. P(s) paren(T;s) P([inl(t)] @ s @ [inr(t)])) (s:(T+T) List. paren(T;s) P(s))	[paren_induction]
0	Thm* a,x:T. (x [a]) x = a	[member_singleton]
2	Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2)	[member_append]