We prove:

with no assumptions.

Proof by sequent calculus with unit propagation:

Equivalence goal MouseOver is proven in both directions.

{1} Direction from left to right: Assume:

and prove:

Disjunctive goal MouseOver is split:

Implicative goal MouseOver is split. Assume:

and prove:

Literal assumption MouseOver is propagated !

Using literal assumption MouseOver, assumption MouseOver is simplified to:

Assumed MouseOver goal MouseOver: success.

{2} Direction from right to left: Assume:

and prove:

Implicative goal MouseOver is split. Assume:

and prove:

Literal goal MouseOver is propagated !

Using literal goal MouseOver, assumption MouseOver is simplified to:

Assumed conjunction MouseOver is split into:

Literal assumption MouseOver is propagated !

Using literal assumption MouseOver, assumption MouseOver is simplified to:

Contradictory assumptions MouseOver, MouseOver: success.