A:Type, eq:EqDecider(A), f:a:A fp-> Top.
Thm* fpf-dom-list(f)
{a:A| a dom(f) } Listeq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) 
(x L)T:Type, L:T List. L {x:T| (x L) } List| Rank | Theorem | Name |
| 3 | A:Type, eq:EqDecider(A), f:a:A fp-> Top.
Thm* fpf-dom-list(f) {a:A| a dom(f) } List | [fpf-dom-list_wf] |
| cites the following: | ||
| 2 | eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) (x L) | [assert-deq-member] |
| 0 | T:Type, L:T List. L {x:T| (x L) } List | [list-set-type] |