Validity checking for combinations of theories with equality