destruct on 'exists' should remove original hypothesis
on hypothesis of the form
H: exists x:t. P
the transformation destruct H
should produce
constant x:t H: P
and should NOT keep the original hypothesis
on hypothesis of the form
H: exists x:t. P
the transformation destruct H
should produce
constant x:t H: P
and should NOT keep the original hypothesis