fv-negt

Theorem.

Arguments:

(sv), (pr),

Assertions:

(()())

Proof:

Hyp	Ref	Line	Expr
	con	1	(()())
1	2im.bldal	2	(()())
	ax6	3	()
3	con<	4	()
2, 4	rpi32	5	(()())