B:(A
Type), B':(A'Type).
Thm* (x:A. B(x)) ~ (x':A'. B'(x'))
(x':A'. B'(x')) ~ (x:A. B(x)) InvFuns(B;A;g;f)| Theorem | Name |
| B:(AType), B':(A'Type).
Thm* (x:A. B(x)) ~ (x':A'. B'(x')) (x':A'. B'(x')) ~ (x:A. B(x)) | [one_one_corr_fams_sym] |
| cites the following: | |
| InvFuns(B;A;g;f) | [inv_funs_2_sym] |