T:S, P:(TProp). (x:T. P(x))  (x:T. P(x))

By:	RewriteOfThm Thm* T:S, P:(T). (x:T. P(x)) = (x:T. P(x)) (SimpsetC [`bequal`])

1

1. T:S, P:(T). (x:T. P(x))  (x:T. P(x))   T:S, P:(TProp). (x:T. P(x))  (x:T. P(x))

1 step

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