IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
filter functionality A:Type, L:A List, f1,f2:(A). f1 = f2 (filter(f1;L) ~ filter(f2;L))
By:
InductionOnList THEN Reduce 0 THEN UnivCD THEN Obvious
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A:Type, L:A List, f1,f2:(A
). f1 = f2 
(filter(f1;L) ~ filter(f2;L))
