PrintForm
Definitions
Lemmas
mb
list
2
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
filter
trivial2
T
:Type,
P
:(
T
),
L
:
T
List. (
x
L
.
P
(
x
))
filter(
P
;
L
) =
L
By:
Auto
THEN
Inst
Thm*
P
:(
T
),
L
:
T
List. (
x
L
.
P
(
x
))
(filter(
P
;
L
) ~
L
) [
T
;
P
;
L
]
THEN
HypSubst -1 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
mb
list
2
Sections
MarkB
generic
Doc
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) = LP:(T), L:T List. (xL.P(x)) (filter(P;L) ~ L) [T;P;L]
