Nuprl - Pf comp_choice 1 1 1 1 1 1 1

1. E: Prop
2. x,y:. Dec(x E y)
3. r:
4. x,y:. (x r y) (x E y)
5. EquivRel x,y:. x r y

(n,k:. (n r k) Min{ x | xrn } = Min{ x | xrk }) & (n:. n r Min{ x | xrn })

By: Analyze 0

Generated subgoals:

1 n,k:. (n r k) Min{ x | xrn } = Min{ x | xrk }

2 n:. n r Min{ x | xrn }

About:

1	`n,k:. (n r k) Min{ x \| xrn } = Min{ x \| xrk }`
2	`n:. n r Min{ x \| xrn }`