(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
1
1
1.
A
: Type
2.
E
:
A
A
Prop
3. EquivRel
a
,
a'
:
A
.
E
(
a
;
a'
)
4.
q
:
A
/
E
5.
x
: {
x
:
A
|
q
=
x
}
<
x
,
x
> = <
q
,
x
>
q
:
A
/
E
{
x
:
A
|
q
=
x
A
/
E
}
By:
Analyze
Generated subgoal:
1
x
=
q
A
/
E
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
A
<x,x> = <q,x> 
q:A/E
{x:A| q = x 
