Nuprl - list 3 jlc LEMMAs for sublist functionality wrt id id list iso

Rank	Theorem	Name
4			Thm* L1,L2:T List, eq1,eq2:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 L1 = L2 L3(~eq1)L4 (L1(eq2)L3 L2(eq2)L4)	[sublist_functionality_wrt_id_id_list_iso]
cites
2			Thm* Discrete{T} (eq1,eq2,eq3:{T}, L1,L2,L3:T List. eq1 = eq2 eq2 = eq3 L1(eq1)L2 L2(eq2)L3 L1(eq3)L3)	[sublist_transitivity]
3			Thm* Discrete{T} (eq:{T}, L,M:T List. L = M L(eq)M)	[sublist_weakening_wrt_identity]