At:
list accum filter T,A:Type, f:(TAT), P:(A), L:A List, s:T. list_accum(s',x'.f(s',x');s;filter(P;L)) ~ list_accum(i,y.if P(y) f(i,y) else i fi;s;L)
By:
InductionOnList
THEN
Reduce 0
THEN
Analyze 0
THEN
Try Trivial
THEN
SplitOnConclITE
THEN
Reduce 0
THEN
EasyHyp
Generated subgoals:
T,A:Type, f:(T
A
), L:A List, s:T. list_accum(s',x'.f(s',x');s;filter(P;L)) ~ list_accum(i,y.if P(y)
f(i,y) else i fi;s;L)