(6steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card
quotient
1
1.
A
: Type
2.
E
:
A
A
Prop
3. EquivRel
a
,
a'
:
A
.
E
(
a
;
a'
)
(
q
:
A
/
E
{
x
:
A
|
q
=
x
}) ~
A
By:
Witness:
qx
.
qx
/
q
,
x
. x |
x
.<
x
,
x
>
Generated subgoal:
1
InvFuns(
q
:
A
/
E
{
x
:
A
|
q
=
x
};
A
;
qx
.
qx
/
q
,
x
. x;
x
.<
x
,
x
>)
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
A
(q:A/E
{x:A| q = x }) ~ A
qx.qx/q,x. x | 
