Implement a saturation tactic to handle universally quantified assumptions

[sonmarcho]

trafficstars

We need a tactic to automatically saturate the context by instantiating assumptions of the shape forall x y, ... with everything they can find in the context (with maybe a given number of rounds). This would have been useful for both the proofs of the hashmap and the proof of the AVL (see for instance this, which could be automated if we had such a tactic).

Basically, if we have the context:

h : forall (x : A) (y : B), P x y
x : A
y0 : B
y1 : B

calling this tactic would introduce:

_ : P x y0
_ : P x y1