instantiate should be able to remove the general hypothesis
Add an optional argument so that on hypothesis:
H : forall x. x = 0
instantiate H 1
generate the following hypotheses (name change and remove hypothesis):
H : 1 = 0
instead of
H : forall x. x = 0
H_inst : 1 = 0