core StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
2Thm* Dec(A (A  A)[dneg_elim_a]
cites the following:
1Thm* Dec(A A  A[dneg_elim]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
core StandardLIB Doc