sb-xpl

Theorem.

Arguments:

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

Hypotheses:

(()())

( bound in )

Assertions:

([/])

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(()())
		2	( bound in )
2	sb-bv	3	([/])
	sb-eqat<x	4	[/]()
1, 4	im.bldsb	5	[/]()
3, 5	sb-bi>	6	([/])