Nuprl - Pf list_quo_choice 2 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))

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

By: Assert (q = 0)

Generated subgoal:

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

About: