IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
one one corr fams wf A,A':Type, B:(AType), B':(A'Type).
((x:A. B(x)) ~ (x':A'. B'(x'))) Prop
By:
Def of ([var]:<type>. <type>) ~ ([var]:<type>. <type>)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A,A':Type, B:(A
Type), B':(A'
((x:A. B(x)) ~ (x':A'. B'(x'))) 
Prop
