Changed subsumption check to handle multiple simultaneous definitions

Previously:

  g : some a c. forall b. a -> b -> c
  g x y = h x y
  h y x = g x y

would pass with:

  g : forall a b c. a -> b -> c
  h : forall a c. a -> a -> c

while:

  h y x = g x y
  g : some a c. forall b. a -> b -> c
  g x y = h x y

would fail with a skolem escape. Now both fail.