No other cites to report in StandardLib
union1_term3	Def union1_term3(x) == inr(inr(x))
	Thm* x:(). union1_term3(x)  union1()

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html