IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
filter trivial2 T:Type, P:(T), L:T List. (xL.P(x)) filter(P;L) = L
By:
Auto
THEN
Inst Thm*P:(T), L:T List. (xL.P(x)) (filter(P;L) ~ L) [T;P;L]
THEN
HypSubst -1 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
T:Type, P:(T
), L:T List. (
L.P(x)) 
filter(P;L) = L
