eqcomi

Theorem.

Arguments:

(st), (st),

Assertions:

(()())

Proof:

Hyp	Ref	Line	Expr
	eqid	1	()
	ax8	2	(()(()()))
1, 2	mpi	3	(()())