Nuprl - Proof: s-pre-init-rule1 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: s-pre-init-rule1 1 1 1 1

1. Id
2. Id
3. x : Id
4. A : Type
5. T : Type
6. A
7. A

Prop
8. x@0:Id

x : A(x@0)?Top

x : A(x)?Top

r A

By:

Reduce 0

Generated subgoals:

None

About:

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