ss.ps

Theorem.

Arguments:

(obj), (obj),

Assertions:

(()(()()))

Proof:

Hyp	Ref	Line	Expr
	df<-alt2	1	((()())())
1	exp	2	(()(()()))
2	con<	3	(()(()()))
3	df-or	4	(()(()()))
	ps→ss	5	(()())
	eq.less<	6	(()())
5, 6	jaoi	7	((()())())
4, 7	>bii	8	(()(()()))