Nuprl - Pf list_quo_choice 2 1 1 1 1

1. q:
2. 0 < q
3. E: q*q*Prop
4. (EquivRel x,y:q*. x E y) & (x,y:q*. Dec(x E y))
5. q = 0

(x,y:q*. (x E y) Id(x) = Id(y) q*) & (x:q*. x E (Id(x)))

By: Analyze 0

Generated subgoals:

1 x,y:q*. (x E y) Id(x) = Id(y) q*

2 x:q*. x E (Id(x))

About: