sb-negw

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Assertions:

([/][/])

Proof:

Hyp	Ref	Line	Expr
	dfsb-dvex	1	([/](()))
1	bi.bldneg	2	([/](()))
	aln.ex	3	((())(()))
2, 3	><bitr	4	((())[/])
	im.nan	5	((())(()))
5	eqt-∀-i	6	((())(()))
	dfsb-dval	7	([/](()))
4, 6, 7	2bitr	8	([/][/])