eqt>

Theorem.

Arguments:

(st), (coll), (coll),

Dummy variables:

(sv),

Distinct variable conditions:

(, ), (, ), (, ),

Assertions:

(()(()()))

Proof:

Hyp	Ref	Line	Expr
	df-equ	1	(()(()()))
1	spec	2	(()[/](()()))
	eqt<	3	(()(()()))
	eqt<	4	(()(()()))
3, 4	bi.bldbi<>d	5	(()((()())(()())))
	ax17-bv	6	( bound in (()()))
5, 6	sb-xplw	7	([/](()())(()()))
2, 7	brpi22	8	(()(()()))