T:Type, P:(T
), L:T List. (x
L.P(x)) 
(filter(P;L) ~ L) T:Type, P:(T), L:T List. (xL.P(x)) (filter(P;L) ~ L)| By: |
THEN Reduce 0 THEN SplitOnConclITE THEN Analyze 0 THEN RWO Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x) & (yL.P(y)) -1 |
| 1 |
2. P : T
3. T List 4. u : T 5. v : T List 6. ( xv.P(x)) (filter(P;v) ~ v)
7. P(u) 8. P(u) & ( xv.P(x))
[u / filter(P;v)] ~ [u / v] | 1 step |
| 2 |
2. P : T
3. T List 4. u : T 5. v : T List 6. ( xv.P(x)) (filter(P;v) ~ v)
7.  P(u)
8. P(u) & ( xv.P(x))
filter(P;v) ~ [u / v] | 1 step |
About:
 |  |  |  |  |  |  |  |  |  |  |