(2steps total) PrintForm Definitions hol Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: choose functionality axiom
  T:S, P,Q:(TType). (x:T. P(x)  Q(x))  (@x:T. P(x)) = (@x:T. Q(x))
By: Id THEN StrongAuto

Generated subgoal:

1   T:S, P,Q:(TType). (x:T. P(x)  Q(x))  (@x:T. P(x)) = (@x:T. Q(x))
1 step

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

(2steps total) PrintForm Definitions hol Sections HOLlib Doc