graph
1
1
Sections
Graphs
Doc
Def
(
x
L.P(x)) == reduce(
x,b. P(x)
b;false
;L)
is mentioned by
Thm*
L:T List, P:(T
). (
x
L.P(x))
(
i:
||L||. P(L[i]))
[assert_l_bexists]
Try larger context:
Graphs
graph
1
1
Sections
Graphs
Doc
L:T List, P:(T
). (
x
L.P(x)) 
(i:
||L||. P(L[i]))xL.P(x)) == reduce(
x,b. P(x) 
b;false;L)
L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i]))