Nuprl - Pf quotient_of

1. E: 11Prop
2. EquivRel x,y:1. x E y
3. x,y:1. Dec(x E y)

f:(1(i,j:1//(i E j))), g:((i,j:1//(i E j))1). InvFuns(1; i,j:1//(i E j); f; g)

By: Assert (0 i,j:1//(i E j))

Generated subgoals:

1 0 i,j:1//(i E j)

2 4. 0 i,j:1//(i E j)
f:(1(i,j:1//(i E j))), g:((i,j:1//(i E j))1). InvFuns(1; i,j:1//(i E j); f; g)

About:

1	`0 i,j:1//(i E j)`
2	4. `0 i,j:1//(i E j)` `f:(1(i,j:1//(i E j))), g:((i,j:1//(i E j))1). InvFuns(1; i,j:1//(i E j); f; g)`