(7steps total) PrintForm NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc some via so 1 1 1

1. A : Type
2. B : AProp
3. x : A
4. B(x)
  C:Prop. (x:AB(x C C


By: Auto


Generated subgoal:

1 5. C : Prop
6. x:AB(x C
  C

1 step

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

(7steps total) PrintForm NuprlPrimitives Sections NuprlLIB Doc