Nuprl - Pf comp_choice 1 1 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
6. n:
7. k:

(n r k) Min{ x | xrn } = Min{ x | xrk }

By: Inst Thm* E:(), n,k:. (EquivRel x,y:. x E y) ((n E k) Min{ x | xEn } = Min{ x | xEk }) [r;n;k]

Generated subgoals:

None

About: