eq:EqDecider(A), f,g:x:A fp-> Top.
Thm* fpf-is-empty(f
g) ~ (fpf-is-empty(f)
fpf-is-empty(g))P:(T
), L:T List. (x
L.P(x)) 
(filter(P;L) ~ L)as,bs:T List. ||as @ bs|| = ||as||+||bs|| 
| Rank | Theorem | Name |
| 4 | eq:EqDecider(A), f,g:x:A fp-> Top.
Thm* fpf-is-empty(f g) ~ (fpf-is-empty(f)fpf-is-empty(g)) | [fpf-join-is-empty] |
| cites the following: | ||
| 3 | P:(T), L:T List. (xL.P(x)) (filter(P;L) ~ L) | [filter_trivial] |
| 0 | as,bs:T List. ||as @ bs|| = ||as||+||bs|| | [length_append] |