let trivial_is_implied a1 a2 = match a1, a2 with | Comp (x1, Neq, Elem (v1, (Constr|Var))), Comp (x2, Eq, Elem (v2, (Constr|Var))) when not (Hstring.equal v1 v2) && Term.compare x1 x2 = 0 -> 0 | _ -> compare a1 a2