There are several ways to do what you want. One of them is to use a different syntax representation under which $\alpha$-equivalent terms are actually equal. Such representations go under the name nameless or locally nameless syntax. A popular one uses de Bruijn indices. See my blog posts How to implement dependent type theory I, II and III for a blitz introduction to implementing this sort of thing (part III has de Bruijn indices explained).
If you insist on your representation, then we may still secretly use de Bruijn indices, as follows. As we descend inside a subterm during comparison, we keep a list of pairs of bound variables so far encountered. For example, when comparing Forall x1 e1 and Forall x2 e2, we add the pair (x1, x2) to the list and recursively compare e1 and e2. When asked to compare variables x and y, we search down the list: either they must both appear in the same spot (they were bound by the same quantifier) or neither appears and they are equal (they are both free and they are equal).
I am not well-versed with Haskell, but you'd get something like this:
newtype Var = Var Int deriving Eq
data Term = Belong Var Var
| Bot
| Imply Term Term
| Forall Var Term
equalVar :: [(Var,Var)] -> Var -> Var -> Bool
equalVar [] x y = (x == y)
equalVar ((x,y):bound) z w = (x == z && y == w) || (x /= z && y /= w && equalVar bound z w)
equal' :: [(Var, Var)] -> Term -> Term -> Bool
equal' bound (Belong x1 y1) (Belong x2 y2) = (equalVar bound x1 x2 && equalVar bound y1 y2)
equal' bound Bot Bot = True
equal' bound (Imply u1 v1) (Imply u2 v2) = equal' bound u1 u2 && equal' bound v1 v2
equal' bound (Forall x u) (Forall y v) = equal' ((x,y):bound) u v
equal' _ _ _ = False
equal :: Term -> Term -> Bool
equal e1 e2 = equal' [] e1 e2
