a,b,a',b':
. (a ~ a') 
(b ~ b') ((a ~ b) 
(a' ~ b'))R:(T
TProp).
Thm* (EquivRel x,y:T. R(x,y))
Thm*
Thm* (
a,a',b,b':T. R(a,b) R(a',b') (R(a,a') R(b,b'))). x ~ y| Rank | Theorem | Name |
| 3 | a,b,a',b':. (a ~ a') (b ~ b') ((a ~ b) (a' ~ b')) | [assoced_functionality_wrt_assoced] |
| cites the following: | ||
| 0 | R:(TTProp).
Thm* (EquivRel x,y:T. R(x,y)) Thm*
Thm* ( a,a',b,b':T. R(a,b) R(a',b') (R(a,a') R(b,b'))) | [equiv_rel_self_functionality] |
| 2 | . x ~ y | [assoced_equiv_rel] |