improve mutual exclusion using neck-guards

[gares]

For the overlapping check in Coq, be careful about the problematic-subterms as in here: the two non unifying terms {{fun x => f (H x)}} and {{fun y => g (G y)}} are both replaced with a uvar combined with a constraint relating the uvar with the original term. Wrt overlapping check, this will cause a compilation error of the DB...