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
La mise à jour de gitlab est terminée. Nous sommes désormais en version 16.11.1
Merci de consulter la release note:
https://about.gitlab.com/releases/2024/04/18/gitlab-16-11-released/
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