B:(A
Type), f:x:A fp-> B(x). fpf-is-empty(f) 
f = 
x:A fp-> B(x)l:T List. ||l|| = 0 
l = nil| Theorem | Name |
| B:(AType), f:x:A fp-> B(x). fpf-is-empty(f) f = x:A fp-> B(x) | [assert-fpf-is-empty] |
| cites the following: | |
| l:T List. ||l|| = 0 l = nil | [length_zero] |