Nuprl - Proof: exists over and r

(3steps total) PrintForm Definitions core StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: exists over and r

T:Type, A:Prop, B:(T

Prop). (

x:T. A & B(x))

A & (

x:T. B(x))

By:

GenExRepD

Generated subgoals:

1 1. T : Type
2. A : Prop
3. B : TProp
4. x : T
5. A
6. B(x)
x:T. B(x)
1 step

2 1. T : Type
2. A : Prop
3. B : TProp
4. A
5. x : T
6. B(x)
x:T. A & B(x)
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(3steps total) PrintForm Definitions core StandardLIB Doc

1	1. T : Type 2. A : Prop 3. B : TProp 4. x : T 5. A 6. B(x) x:T. B(x)	1 step
2	1. T : Type 2. A : Prop 3. B : TProp 4. A 5. x : T 6. B(x) x:T. A & B(x)	1 step