Deeplim inverses some equalities when sections are involved

[thomas-lamiaux]

I found a weird behavior with depelim. In the code below, depelim keeps inverting the equality

Section Foo.
  Context (x y : vec nat 2).

Definition foo (H : x = y) : x = y.
  depelim H.
  depelim H.
  depelim H.

but with this code, the equality gets deleted

Definition foo (x y : vec nat 2) (H : x = y) : x = y.
  depelim H.