(2steps total) PrintForm Definitions mb event system 3 Sections EventSystems Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: subtype-fpf2
  A:Type, B1,B2:(AType).
  (a:A. B1(a) r B2(a))  (a:A fp-> B1(a) r a:A fp-> B2(a))
By: Auto THEN Analyze 0 THEN ParallelOp -1 THEN Analyze -1 THEN Analyze

Generated subgoal:

1 1. A : Type
2. B1 : AType
3. B2 : AType
4. a:A. B1(a) r B2(a)
5. d : A List
6. a:{a:A| (a  d) }B1(a)
7. x2 : {a:A| (a  d) }
  (B1(x2))  (B2(x2))
1 step

About:
applyfunctionuniversesubtypesubtype_relimpliesall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(2steps total) PrintForm Definitions mb event system 3 Sections EventSystems Search Doc