IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
filter filter T:Type, P1,P2:(T), L:T List.
filter(P1;filter(P2;L)) ~ filter(t.(P1(t))(P2(t));L)
By:
ObviousListInduction
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T:Type, P1,P2:(T
), L:T List.
filter(P1;filter(P2;L)) ~ filter(
t.(P1(t))
(P2(t));L)
