ax16-bv

Theorem.

Arguments:

(sv), (st), (pr),

Distinct variable conditions:

(, ),

Assertions:

(()( bound in ))

Proof:

Hyp	Ref	Line	Expr
	ax16	1	(()())
	df-Bvp	2	(( bound in )())
1, 2	brpi22<	3	(()( bound in ))