Def  (x:A. B(x)) ~ (x':A'. B'(x'))
Def  == f:(AA'), g:(A'A), F:(x:AB(x)B'(f(x))), G:(x:AB'(f(x))B(x)).
Def  == InvFuns(A;A';f;g) & (u:A. InvFuns(B(u);B'(f(u));F(u);G(u)))

is mentioned by

Thm*  (x:A. B(x)) ~ (x:A'. B'(x))  ((x:AB(x)) ~ (x:A'B'(x)))	[card_pi]
Thm*  (x:A. B(x)) ~ (x:A'. B'(x))  ((x:AB(x)) ~ (x:A'B'(x)))	[card_sigma]
Thm*  (A ~ A')  (B ~ B')  (:A. B) ~ (:A'. B')	[one_one_corr_fams_indep_if_one_one_corr]
Thm*  g:(A'A). Bij(A'; A; g)  (x:A. B(x)) ~ (x':A'. B(g(x')))	[one_one_corr_fams_if_bij_A]
Thm*  (x:A. B(x) ~ B'(x))  (x:A. B(x)) ~ (x:A. B'(x))	[one_one_corr_fams_if_one_one_corr_B]
Thm*  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]
Thm*  A:Type, A',A'':Type, B:(AType), B':(A'Type), B'':(A''Type). Thm*  (x:A. B(x)) ~ (x':A'. B'(x')) Thm*   Thm*  (x':A'. B'(x')) ~ (x'':A''. B''(x''))  (x:A. B(x)) ~ (x'':A''. B''(x''))	[one_one_corr_fams_trans]
Thm*  (x:A. B(x)) ~ (x:A. B(x))	[one_one_corr_fams_refl]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html