At:
mapfilter append
T:Type, P:(T
), T':Type, f:({x:T| P(x) }T'), L1,L2:T List. mapfilter(f;P;L1 @ L2) = (mapfilter(f;P;L1) @ mapfilter(f;P;L2))
By:
InductionOnList
THEN
Reduce 0
THEN
Unfold `mapfilter` 0
THEN
Reduce 0
THEN
Repeat SplitOnConclITE
THEN
Reduce 0
THEN
Fold `mapfilter` 0
THEN
Obvious
Generated subgoals:
None
About:
