Demonstrate strange rewrite behavior

rewrite_drops_hyps.v

Require Import List.
Import ListNotations.
Require Import ssreflect.
Lemma test1 :
  length ([1] ++ [2]) = 2 ->
  2 = 4.
Proof.
  intros HA.
  evar (N : nat).
  Unshelve.
  admit.
  Check HA.
  Undo.
  Undo.
  rewrite -> app_length in HA.
  Unshelve.
  admit.
  (* Now [HA] has disappeared from the context of the second goal, unless we run [clear N]. *)
  Fail Check HA.
Abort.


Lemma test2 :
  length ([1] ++ [2]) = 2 ->
  exists n : nat, n + 4 = 2.
Proof.
  intros HA.
  eexists.
  Unshelve.
  admit.
  Check HA.
  Undo.
  Undo.
  rewrite /= in HA.
  Unshelve.
  admit.
  (* Now [HA] has disappeared from the context of the second goal, and we can't [clear N] to fix that. *)
  Fail Check HA.
Abort.