(6steps total)
PrintForm
Definitions
quot
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
quotient
wf
T
:Type,
E
:(
T
T
Prop). (EquivRel
x
,
y
:
T
.
E
(
x
,
y
))
x
,
y
:
T
//
E
(
x
,
y
)
Type
By:
UnivCD
Generated subgoal:
1
1.
T
: Type
2.
E
:
T
T
Prop
3. EquivRel
x
,
y
:
T
.
E
(
x
,
y
)
x
,
y
:
T
//
E
(
x
,
y
)
Type
5
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
quot
1
Sections
StandardLIB
Doc
T:Type, E:(T
TProp). (EquivRel x,y:T. E(x,y)) 
x,y:T//E(x,y) 
Type T:Type, E:(TTProp). (EquivRel x,y:T. E(x,y)) x,y:T//E(x,y) TypeTProp
x,y:T//E(x,y) Type
