(* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements
* (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *)
(* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements
* (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *)