(2steps total)
PrintForm
Definitions
rel
1
Sections
StandardLIB
Search
Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
equiv
rel
iff
EquivRel
A
,
B
:Prop.
A
B
By:
Unfold `equiv_rel` 0
Generated subgoal:
1
Refl(Prop;
A
,
B
.
A
B
) & (Sym
A
,
B
:Prop.
A
B
) & (Trans
A
,
B
:Prop.
A
B
)
1
step
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
rel
1
Sections
StandardLIB
Search
Doc
EquivRel A,B:Prop. A 
B EquivRel A,B:Prop. A B Refl(Prop;A,B.A B) & (Sym A,B:Prop. A B) & (Trans A,B:Prop. A B)
