sb-bi>

Theorem.

Arguments:

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

Hypotheses:

([/])

Assertions:

([/]()([/]))

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	([/])
	sb-bi	2	([/]()([/][/]))
1	bi.bldbi>	3	(([/][/])([/]))
2, 3	bitr	4	([/]()([/]))