IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
filter map T1,T2:Type, f:(T1T2), Q:(T2), L:T1 List.
filter(Q;map(f;L)) = map(f;filter(Q o f;L))
By:
InductionOnList THEN Reduce 0 THEN SplitOnConclITE THEN Reduce 0 THEN Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T1,T2:Type, f:(T1
T2), Q:(T2
), L:T1 List.
filter(Q;map(f;L)) = map(f;filter(Q o f;L))
