(8steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: one one corr is equiv rel
  EquivRel X,Y:Type. X ~ Y
By: Def of X ~ Y THEN BackThru: equivrel characterization

Generated subgoals:

1 1. X : Type
  f,g:(XX). InvFuns(X;X;f;g)
1 step
2 1. X : Type
2. Y : Type
3. f:(XY), g:(YX). InvFuns(X;Y;f;g)
  g:(YX), f:(XY). InvFuns(Y;X;g;f)
1 step
3 1. X : Type
2. Y : Type
3. f1:(XY), g1:(YX). InvFuns(X;Y;f1;g1)
4. Z : Type
5. f2:(YZ), g2:(ZY). InvFuns(Y;Z;f2;g2)
  f:(XZ), g:(ZX). InvFuns(X;Z;f;g)
5 steps

About:
functionuniverseexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(8steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc