Nuprl - Proof: da-outlinks-empty

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: da-outlinks-empty

ltg:(IdLnk

Type), i:Id. (ltg

da-outlinks(;i))

False

By:	Repeat (Unfolds ([`fpf-dom-list` (;`da-outlinks` (;`fpf-empty` (;`mapfilter` (;`l_member` (;`da-outlink-f`] (0 (THEN (Reduce 0) THEN ExRepD

Generated subgoals:

None

About:

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