Nuprl - Proof: inhab rep eqv

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: inhab rep eqv

F:(Prop{i}

Prop{j}). (

P:Prop{i}. F(P))

(

A:Type{i}. F(

A))

By:

Auto

Generated subgoals:

1 1. F : Prop{i}Prop{j}
2. P:Prop{i}. F(P)
3. A : Type{i}
F(A)
1 step

2 1. F : Prop{i}Prop{j}
2. A:Type{i}. F(A)
3. P : Prop{i}
F(P)
3 steps

About:

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

1	1. F : Prop{i}Prop{j} 2. P:Prop{i}. F(P) 3. A : Type{i} F(A)	1 step
2	1. F : Prop{i}Prop{j} 2. A:Type{i}. F(A) 3. P : Prop{i} F(P)	3 steps