Who Cites rev implies?
rev_implies	Def P Q == Q P
	Thm* A,B:Prop. (A B) Prop

Syntax:

P Q

has structure:

rev_implies(P; Q)

About: