BooleanFormula implies is wrong

The current implementation looks like this:

implies :: Eq a => BooleanFormula a -> BooleanFormula a -> Bool
x `implies` Var y  = x `impliesAtom` y
x `implies` And ys = all (implies x . unLoc) ys
x `implies` Or ys  = any (implies x . unLoc) ys
x `implies` Parens y  = x `implies` (unLoc y)

This cannot possibly be correct: this will decompose the formula A \/ B -> A \/ B in the following way

Or [Var a, Var b] `implies` Or [Var a, Var b]

Or [Var a, Var b] `implies` Var a ||
Or [Var a, Var b] `implies` Var b

But neither of the decomposed formulas are true, so GHC will never find a proof.

I didn't find a case in the typechecker where this actually mattered.