Nuprl - Proof: fpf-dom-list wf

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fpf-dom-list wf

A:Type, eq:EqDecider(A), f:a:A fp-> Top.

fpf-dom-list(f)

{a:A| a

dom(f) } List

By:	Auto THEN DVar `f' THEN Unfolds [`fpf-dom-list`;`fpf-dom`] 0 THEN Reduce 0 THEN Inst Thm* T:Type, L:T List. L {x:T\| (x L) } List [A;d] THEN DoSubsume THEN UseSubtypeRelLemmas THEN Analyze 0 THEN Analyze -1 THEN Analyze THEN RWO Thm* eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) (x L) 0

Generated subgoals:

None

About:

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