df-bvt
Definition.
Arguments:
(sv),
(coll),
(sv),
Distinct variable conditions:
(
,
), (
,
),
Assertions:
((
bound in
)
(
bound in (
)))
(sv), 
(coll), 
(sv), (sv), (coll), (sv), , ), (, ), bound in )
( bound in (
)))