(16steps total) PrintForm Definitions LogicSupplement Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A compact characterization of equivalence relations.

At: equivrel characterization

  A:Type, R:(AAProp).
  (EquivRel x,y:A. R(x,y))
  
  (x:A. R(x,x) & (y:A. R(x,y)  R(y,x) & (z:A. R(y,z)  R(x,z))))
By: UnivCD THEN Analyze 0 THEN Analyze 0

Generated subgoals:

1 1. A : Type
2. R : AAProp
3. EquivRel x,y:A. R(x,y)
  x:A. R(x,x) & (y:A. R(x,y)  R(y,x) & (z:A. R(y,z)  R(x,z)))
7 steps
2 1. A : Type
2. R : AAProp
3. x:A. R(x,x) & (y:A. R(x,y)  R(y,x) & (z:A. R(y,z)  R(x,z)))
  EquivRel x,y:A. R(x,y)
8 steps

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

(16steps total) PrintForm Definitions LogicSupplement Sections DiscrMathExt Doc