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