(3steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
assoced
equiv
rel
1
EquivRel
x
,
y
:
. Symmetrize(
u
,
v
.
u
|
v
;
x
;
y
)
By:
Backchain
[
Thm*
R
:(
T
T
Prop).
[Thm*
Preorder(
T
;
x
,
y
.
R
(
x
,
y
))
(EquivRel
a
,
b
:
T
. Symmetrize(
x
,
y
.
R
(
x
,
y
);
a
;
b
))
;
Thm*
Preorder(
;
x
,
y
.
x
|
y
)]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
EquivRel x,y:
. Symmetrize(u,v.u | v;x;y) EquivRel x,y:. Symmetrize(u,v.u | v;x;y)
R:(T
TProp).
(EquivRel a,b:T. Symmetrize(x,y.R(x,y);a;b))
;x,y.x | y)]
