Nuprl - mb_event_system_6 LEMMAs for ma_DASH_join_DASH_list_DASH

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
8	Thm* L:MsgA List. Thm* (A,BL.A \|\|+ B) (L) MsgA & (M:MsgA. (BL.M \|\|+ B) M \|\|+ (L))	[ma-join-list-property]
cites the following:
0	Thm* A:MsgA. ma-sframe-compatible(A; )	[ma-empty-sframe-compatible-right]
0	Thm* A:MsgA. ma-frame-compatible(A; )	[ma-empty-frame-compatible-right]
1	Thm* A:MsgA. A \|\|	[ma-empty-compatible-right]
1	Thm* T:Type{i}, x:T, L:T List, P:(TTProp{i'}). Thm* (x,y[x / L].P(x,y)) (x,yL.P(x,y)) & (yL.P(x,y))	[pairwise-cons]
7	Thm* A,B,C:MsgA. A \|\|+ B C \|\|+ A C \|\|+ B C \|\|+ A B	[ma-compat-join]
2	Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) & (yL.P(y))	[l_all_cons]

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html