Nuprl - Proof: exteq sum family singleton vs intseg 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: exteq sum family singleton vs intseg 1 2

1. a :

2. a' :

3. a'-a = 1
4. B : {a..a'

}

Type
5. i : {a:

}
6. b : B(a)

B(i)

By:

Analyze-2

Generated subgoal:

1 5. i :
6. i = a
7. b : B(a)
b B(i)
2 steps

About:

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