PrintForm Definitions mb list 1 Sections MarkB generic Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/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:
listboollambdaapplyfunctionuniversesqequalall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions mb list 1 Sections MarkB generic Search Doc