T:Type, P:(T
), T':Type, f:({x:T| P(x) }T'), L:T List, x,y:{x:T| P(x) }. x before y 
L 
f(x) before f(y) mapfilter(f;P;L)
Try (ExtWith [`z'] [T]) in
((((Auto
THEN
(All
(RWO
Thm* L:T List, x,y:T. x before y L 
(
L1,L2,L3:T List. L = (L1 @ [x] @ L2 @ [y] @ L3))))
THEN
ExRepD
THEN
(HypSubst -1 0)
THEN
(RWW
Thm* 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))
0))
THENA
(Auto THEN tac))
THEN
(InstConcl [mapfilter(f;P;L1);mapfilter(f;P;L2);mapfilter(f;P;L3)]))
THENA
(Auto THEN tac))
THEN
(Repeat Analyze)
THEN
(Unfold `mapfilter` 0)
THEN
(Reduce 0)
THEN
SplitOnConclITE
THEN
(Reduce 0)
THEN
(Analyze -1)
THEN
(AllHyps (
h.(Analyze h) THEN Unhide THEN (Complete Auto)))
None
About:
| | | | | | |
 |  |  |  |  |
 |