Issue title: cases produces extra hypothesis
 Issue body: Sometimes the `cases` tactic produces a new "useless" hypothesis. For example, in the next example the hypothesis `e_2 : refl y = refl y` is generated.

```
open eq

definition foo {A : Type} (P : A → Type) {x y : A} (p : x = y) {a : P x} 
{b : P y} (q : p ▹ a = b) : A :=
begin
  cases p, clear e_2, exact x
end
```

 Comments: 
 Comment 0: PS: in the above case the variable `p` is also not removed from the context. 

Also, when you do cases on `p : x = y`, in future hypotheses/goals all variables `x` are replaced by `y` (and `p` by `refl y`). It would be nice if `x` is also removed from the context.

 Comment 1: The `cases` tactic is quite complicated in HoTT mode.
It performs a sequence of steps. The auxiliary hypotheses are generated in the process. When they are generated, they are not trivial. They become trivial later. 
Some of them are easy to remove (e.g., the one in `foo`). I submitted a fix that removes the easy ones.
To get rid of all of them, I think the only solution is a post-processor. 
Something that would go over the hypotheses and remove the ones of the form `(H : a = a)`.

{'source': 'GithubIssues', 'repo_name_with_owner': 'leanprover/lean', 'issue_id': 60739046, 'repo_stars': 2077.0}