Nuprl - list 3 jlc LEMMAs for append functionality wrt list iso

Rank	Theorem	Name
2			Thm* L1,L2:T List, eq1,eq2,eq3:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 eq2 = eq3 L1(~eq1)L2 L3(~eq2)L4 (L1 @ L3)(~eq3)(L2 @ L4)	[append_functionality_wrt_list_iso]
cites
1			Thm* L1,L2:T List, eq1,eq2,eq3:{T}, L3,L4:T List. Discrete{T} eq1 = eq2 eq2 = eq3 L1(eq1)L2 L3(eq2)L4 (L1 @ L3)(eq3)(L2 @ L4)	[append_functionality_wrt_sublist]