let rec eq s t =
  match s, t with  
    | Uninterp(x), Uninterp(y) -> Name.eq x y 
    | Arith(f), Arith(g) -> eq_arith f g 
    | Pair(f), Pair(g) -> eq_pair f g
    | Coproduct(op1), Coproduct(op2) -> op1 = op2
    | Bv(f), Bv(g) -> eq_bv f g
    | Pp(f), Pp(g) -> eq_pp f g
    | Fun(f), Fun(g) -> eq_apply f g
    | Bvarith(f), Bvarith(g) -> eq_interp f g
    | Arrays(f), Arrays(g) -> eq_arrays f g
    | _ -> false

and eq_interp f g =
  match f, g with
    | Unsigned, Unsigned -> true

and eq_bv f g = 
  match f, g with
    | Const(b1), Const(b2) -> 
        Pervasives.compare b1 b2 = 0
    | Conc(n1,m1), Conc(n2,m2) ->
        n1 = n2 && m1 = m2
    | Sub(n1,i1,j1), Sub(n2,i2,j2) ->
        n1 = n2 && i1 = i2 && j1 = j2
    | Bitwise(n1), Bitwise n2 ->
        n1 = n2
    | _ -> false

and eq_pair f g = (f = g)

and eq_apply f g =
  match f, g with
    | Apply _, Apply _ -> true
    | Abs, Abs -> true
    | _ -> false

and eq_arith f g =
  match f, g with
    | Num(q1), Num(q2) -> Q.equal q1 q2
    | Multq(q1), Multq(q2)  -> Q.equal q1 q2
    | Add, Add -> true
    | _ -> false

and eq_arrays f g =
  match f, g with
    | Create, Create -> true
    | Select, Select -> true
    | Update, Update -> true
    | _ -> false

and eq_pp f g =
  match f, g with
    | Expt(n), Expt(m) -> n = m
    | Mult, Mult -> true
    | _ -> false