sb-orw

Theorem.

Arguments:

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

Distinct variable conditions:

(, ),

Assertions:

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

Proof:

Hyp	Ref	Line	Expr
	dfsb-dvex	1	([/]()(()()))
	an.ordi<	2	((()())((())(())))
2	eqt-∃-i	3	((()())((())(())))
	ex.ordi	4	(((())(()))((())(())))
1, 3, 4	2bitr	5	([/]()((())(())))
	dfsb-dvex	6	([/](()))
	dfsb-dvex	7	([/](()))
6, 7	bi.bldor<>	8	(([/][/])((())(())))
5, 8	><bitr	9	([/]()([/][/]))