eq:EqDecider(A), B:(A
Type), f,g,h:a:A fp-> B(a).
Thm* f || h
g || h f 
g || heq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a).
Thm* h || f
h || g h || f geq:EqDecider(A), B:(AType), f,g:a:A fp-> B(a). f || g g || f| Rank | Theorem | Name |
| 6 | eq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a).
Thm* f || h g || h f g || h | [fpf-compatible-join2] |
| cites the following: | ||
| 5 | eq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a).
Thm* h || f h || g h || f g | [fpf-compatible-join] |
| 0 | eq:EqDecider(A), B:(AType), f,g:a:A fp-> B(a). f || g g || f | [fpf-compatible-symmetry] |