let eq x y =
  match x, y with
    | External(n, d), External(m, e) -> 
        Name.eq n m && d = e
    | Rename(n, i, d), Rename(m, j, e) -> 
        Name.eq n m && i = j && d = e
    | Fresh(n, i, d), Fresh(m, j, e) -> 
        Name.eq n m && i = j && d = e
    | Bound(n), Bound(m) ->
        n = m
    | Slack(i, alpha, d), Slack(j, beta, e) ->
        i = j && alpha = beta && d = e
    | _ -> 
        false