df-psub
Definition.
Arguments:
(st),
(st),
Assertions:
((
)
((
)
(
)))
(st), 
(st), (st), (st), 
)
((
)
(
)))