let eq a b =
  match a, b with
    | True, True -> true
    | False, False -> true
    | Equal(a1, b1), Equal(a2, b2) -> Term.eq a1 a2 && Term.eq b1 b2
    | In(a1, d1), In(a2, d2) -> Term.eq a1 a2 && Sign.eq d1 d2
    | _ -> false