IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
choose functionality axiom1 T:S, P,Q:(TType). (x:T. P(x) Q(x)) (@x:T. P(x)) = (@x:T. Q(x))
By:
UseWitness * THEN Fiat
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T:S, P,Q:(T
Type). (
Q(x)) 
