Nuprl - Proof: card quotient 1 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card quotient 1 1 1 1 1

1. A : Type
2. E : A

Prop
3. EquivRel a,a':A. E(a;a')
4. q : A/E
5. x : {x:A| q = x }

x = q

A/E

By:

Analyze5

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html