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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information