E:(T
TProp), E':(T'T'Prop).
Thm* T = T'
Thm*
Thm* (
x,y:T. E(x,y) 
E'(x,y))
Thm*
Thm* ((EquivRel x,y:T. E(x,y))
(EquivRel x,y:T'. E'(x,y))) B| Theorem | Name |
| E:(TTProp), E':(T'T'Prop).
Thm* T = T' Thm*
Thm* ( x,y:T. E(x,y) E'(x,y))
Thm*
Thm* ((EquivRel x,y:T. E(x,y)) (EquivRel x,y:T'. E'(x,y))) | [equiv_rel_functionality_wrt_iff] |
| cites the following: | |
| B | [equiv_rel_iff] |