IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
spread to pi121 1. A : Type
2. B : AType
3. p : x:AB(x)
4. C : Type
5. b : x:AB(x)C (p/x,y. b(x,y)) = b(1of(p),2of(p))
By:
Analyze 3 THEN AbReduce 0
Generated subgoal:
1
3. x : A 4. p1 : B(x)
5. C : Type
6. b : x:AB(x)C b(x,p1) = b(x,p1)
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Type
B(x)
(p/x,y. b(x,y)) = b(1of(p),2of(p))
